Diff of the two buildlogs: -- --- b1/build.log 2020-09-22 19:26:39.270321261 +0000 +++ b2/build.log 2020-09-22 19:43:44.018596004 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Mon Oct 25 13:34:26 -12 2021 -I: pbuilder-time-stamp: 1635212066 +I: Current time: Wed Sep 23 09:26:45 +14 2020 +I: pbuilder-time-stamp: 1600802805 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/buster-reproducible-base.tgz] I: copying local configuration @@ -18,7 +18,7 @@ I: Extracting source gpgv: unknown type of key resource 'trustedkeys.kbx' gpgv: keyblock resource '/root/.gnupg/trustedkeys.kbx': General error -gpgv: Signature made Tue Aug 29 11:05:09 2017 -12 +gpgv: Signature made Wed Aug 30 13:05:09 2017 +14 gpgv: using RSA key B845CE510F9B714D gpgv: Can't check signature: No public key dpkg-source: warning: failed to verify signature on ./hol88_2.02.19940316-35.dsc @@ -30,138 +30,172 @@ dpkg-source: info: applying FTBFS_detection_fix I: using fakeroot in build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/5314/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/22984/tmp/hooks/D01_modify_environment starting +debug: Running on profitbricks-build12-i386. +I: Changing host+domainname to test build reproducibility +I: Adding a custom variable just for the fun of it... +I: Changing /bin/sh to bash +Removing 'diversion of /bin/sh to /bin/sh.distrib by dash' +Adding 'diversion of /bin/sh to /bin/sh.distrib by bash' +Removing 'diversion of /usr/share/man/man1/sh.1.gz to /usr/share/man/man1/sh.distrib.1.gz by dash' +Adding 'diversion of /usr/share/man/man1/sh.1.gz to /usr/share/man/man1/sh.distrib.1.gz by bash' +I: Setting pbuilder2's login shell to /bin/bash +I: Setting pbuilder2's GECOS to second user,second room,second work-phone,second home-phone,second other +I: user script /srv/workspace/pbuilder/22984/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/22984/tmp/hooks/D02_print_environment starting I: set - BUILDDIR='/build' - BUILDUSERGECOS='first user,first room,first work-phone,first home-phone,first other' - BUILDUSERNAME='pbuilder1' - BUILD_ARCH='i386' - DEBIAN_FRONTEND='noninteractive' - DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=18' - DISTRIBUTION='' - HOME='/root' - HOST_ARCH='i386' + BASH=/bin/sh + BASHOPTS=checkwinsize:cmdhist:complete_fullquote:extquote:force_fignore:globasciiranges:hostcomplete:interactive_comments:progcomp:promptvars:sourcepath + BASH_ALIASES=() + BASH_ARGC=() + BASH_ARGV=() + BASH_CMDS=() + BASH_LINENO=([0]="12" [1]="0") + BASH_SOURCE=([0]="/tmp/hooks/D02_print_environment" [1]="/tmp/hooks/D02_print_environment") + BASH_VERSINFO=([0]="5" [1]="0" [2]="3" [3]="1" [4]="release" [5]="i686-pc-linux-gnu") + BASH_VERSION='5.0.3(1)-release' + BUILDDIR=/build + BUILDUSERGECOS='second user,second room,second work-phone,second home-phone,second other' + BUILDUSERNAME=pbuilder2 + BUILD_ARCH=i386 + DEBIAN_FRONTEND=noninteractive + DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=10' + DIRSTACK=() + DISTRIBUTION= + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=i686 + HOST_ARCH=i386 IFS=' ' - INVOCATION_ID='f8232019e8d24e5aa009d4ba83989948' - LANG='C' - LANGUAGE='en_US:en' - LC_ALL='C' - LD_LIBRARY_PATH='/usr/lib/libeatmydata' - LD_PRELOAD='libeatmydata.so' - MAIL='/var/mail/root' - OPTIND='1' - PATH='/usr/sbin:/usr/bin:/sbin:/bin:/usr/games' - PBCURRENTCOMMANDLINEOPERATION='build' - PBUILDER_OPERATION='build' - PBUILDER_PKGDATADIR='/usr/share/pbuilder' - PBUILDER_PKGLIBDIR='/usr/lib/pbuilder' - PBUILDER_SYSCONFDIR='/etc' - PPID='5314' - PS1='# ' - PS2='> ' + INVOCATION_ID=f7eeeb8abb874bd0b462f52ef548c770 + LANG=C + LANGUAGE=de_CH:de + LC_ALL=C + LD_LIBRARY_PATH=/usr/lib/libeatmydata + LD_PRELOAD=libeatmydata.so + MACHTYPE=i686-pc-linux-gnu + MAIL=/var/mail/root + OPTERR=1 + OPTIND=1 + OSTYPE=linux-gnu + PATH=/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path + PBCURRENTCOMMANDLINEOPERATION=build + PBUILDER_OPERATION=build + PBUILDER_PKGDATADIR=/usr/share/pbuilder + PBUILDER_PKGLIBDIR=/usr/lib/pbuilder + PBUILDER_SYSCONFDIR=/etc + PIPESTATUS=([0]="0") + POSIXLY_CORRECT=y + PPID=22984 PS4='+ ' - PWD='/' - SHELL='/bin/bash' - SHLVL='2' - SUDO_COMMAND='/usr/bin/timeout -k 18.1h 18h /usr/bin/ionice -c 3 /usr/bin/nice /usr/sbin/pbuilder --build --configfile /srv/reproducible-results/rbuild-debian/tmp.kbE51YMX2t/pbuilderrc_sfqH --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/buster-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/tmp.kbE51YMX2t/b1 --logfile b1/build.log hol88_2.02.19940316-35.dsc' - SUDO_GID='112' - SUDO_UID='107' - SUDO_USER='jenkins' - TERM='unknown' - TZ='/usr/share/zoneinfo/Etc/GMT+12' - USER='root' - _='/usr/bin/systemd-run' - http_proxy='http://85.184.249.68:3128' + PWD=/ + SHELL=/bin/bash + SHELLOPTS=braceexpand:errexit:hashall:interactive-comments:posix + SHLVL=3 + SUDO_COMMAND='/usr/bin/timeout -k 24.1h 24h /usr/bin/ionice -c 3 /usr/bin/nice -n 11 /usr/bin/unshare --uts -- /usr/sbin/pbuilder --build --configfile /srv/reproducible-results/rbuild-debian/tmp.kbE51YMX2t/pbuilderrc_X78B --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/buster-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/tmp.kbE51YMX2t/b2 --logfile b2/build.log hol88_2.02.19940316-35.dsc' + SUDO_GID=112 + SUDO_UID=107 + SUDO_USER=jenkins + TERM=unknown + TZ=/usr/share/zoneinfo/Etc/GMT-14 + UID=0 + USER=root + _='I: set' + http_proxy=http://78.137.99.97:3128 I: uname -a - Linux profitbricks-build16-i386 4.19.0-10-amd64 #1 SMP Debian 4.19.132-1 (2020-07-24) x86_64 GNU/Linux + Linux i-capture-the-hostname 4.19.0-10-686-pae #1 SMP Debian 4.19.132-1 (2020-07-24) i686 GNU/Linux I: ls -l /bin total 5476 - -rwxr-xr-x 1 root root 1302248 Apr 17 2019 bash - -rwxr-xr-x 3 root root 38280 Jul 10 2019 bunzip2 - -rwxr-xr-x 3 root root 38280 Jul 10 2019 bzcat - lrwxrwxrwx 1 root root 6 Jul 10 2019 bzcmp -> bzdiff - -rwxr-xr-x 1 root root 2227 Jul 10 2019 bzdiff - lrwxrwxrwx 1 root root 6 Jul 10 2019 bzegrep -> bzgrep - -rwxr-xr-x 1 root root 4877 Jun 24 2019 bzexe - lrwxrwxrwx 1 root root 6 Jul 10 2019 bzfgrep -> bzgrep - -rwxr-xr-x 1 root root 3641 Jul 10 2019 bzgrep - -rwxr-xr-x 3 root root 38280 Jul 10 2019 bzip2 - -rwxr-xr-x 1 root root 17768 Jul 10 2019 bzip2recover - lrwxrwxrwx 1 root root 6 Jul 10 2019 bzless -> bzmore - -rwxr-xr-x 1 root root 1297 Jul 10 2019 bzmore - -rwxr-xr-x 1 root root 38692 Feb 28 2019 cat - -rwxr-xr-x 1 root root 75588 Feb 28 2019 chgrp - -rwxr-xr-x 1 root root 63268 Feb 28 2019 chmod - -rwxr-xr-x 1 root root 75588 Feb 28 2019 chown - -rwxr-xr-x 1 root root 153732 Feb 28 2019 cp - -rwxr-xr-x 1 root root 132820 Jan 17 2019 dash - -rwxr-xr-x 1 root root 120676 Feb 28 2019 date - -rwxr-xr-x 1 root root 92040 Feb 28 2019 dd - -rwxr-xr-x 1 root root 100620 Feb 28 2019 df - -rwxr-xr-x 1 root root 149736 Feb 28 2019 dir - -rwxr-xr-x 1 root root 79412 Jan 9 2019 dmesg - lrwxrwxrwx 1 root root 8 Sep 26 2018 dnsdomainname -> hostname - lrwxrwxrwx 1 root root 8 Sep 26 2018 domainname -> hostname - -rwxr-xr-x 1 root root 34532 Feb 28 2019 echo - -rwxr-xr-x 1 root root 28 Jan 7 2019 egrep - -rwxr-xr-x 1 root root 34532 Feb 28 2019 false - -rwxr-xr-x 1 root root 28 Jan 7 2019 fgrep - -rwxr-xr-x 1 root root 67700 Jan 9 2019 findmnt - -rwsr-xr-x 1 root root 30112 Apr 22 2020 fusermount - -rwxr-xr-x 1 root root 206392 Jan 7 2019 grep - -rwxr-xr-x 2 root root 2345 Jan 5 2019 gunzip - -rwxr-xr-x 1 root root 6375 Jan 5 2019 gzexe - -rwxr-xr-x 1 root root 100952 Jan 5 2019 gzip - -rwxr-xr-x 1 root root 21916 Sep 26 2018 hostname - -rwxr-xr-x 1 root root 79752 Feb 28 2019 ln - -rwxr-xr-x 1 root root 55400 Jul 26 2018 login - -rwxr-xr-x 1 root root 149736 Feb 28 2019 ls - -rwxr-xr-x 1 root root 112032 Jan 9 2019 lsblk - -rwxr-xr-x 1 root root 87972 Feb 28 2019 mkdir - -rwxr-xr-x 1 root root 79748 Feb 28 2019 mknod - -rwxr-xr-x 1 root root 46916 Feb 28 2019 mktemp - -rwxr-xr-x 1 root root 42348 Jan 9 2019 more - -rwsr-xr-x 1 root root 50592 Jan 9 2019 mount - -rwxr-xr-x 1 root root 13724 Jan 9 2019 mountpoint - -rwxr-xr-x 1 root root 157832 Feb 28 2019 mv - lrwxrwxrwx 1 root root 8 Sep 26 2018 nisdomainname -> hostname - lrwxrwxrwx 1 root root 14 Feb 14 2019 pidof -> /sbin/killall5 - -rwxr-xr-x 1 root root 38660 Feb 28 2019 pwd - lrwxrwxrwx 1 root root 4 Apr 17 2019 rbash -> bash - -rwxr-xr-x 1 root root 46852 Feb 28 2019 readlink - -rwxr-xr-x 1 root root 75588 Feb 28 2019 rm - -rwxr-xr-x 1 root root 42756 Feb 28 2019 rmdir - -rwxr-xr-x 1 root root 22276 Jan 21 2019 run-parts - -rwxr-xr-x 1 root root 125036 Dec 22 2018 sed - lrwxrwxrwx 1 root root 4 Oct 24 02:48 sh -> dash - -rwxr-xr-x 1 root root 34532 Feb 28 2019 sleep - -rwxr-xr-x 1 root root 79652 Feb 28 2019 stty - -rwsr-xr-x 1 root root 71072 Jan 9 2019 su - -rwxr-xr-x 1 root root 34564 Feb 28 2019 sync - -rwxr-xr-x 1 root root 504024 Apr 23 2019 tar - -rwxr-xr-x 1 root root 13860 Jan 21 2019 tempfile - -rwxr-xr-x 1 root root 104292 Feb 28 2019 touch - -rwxr-xr-x 1 root root 34532 Feb 28 2019 true - -rwxr-xr-x 1 root root 17768 Apr 22 2020 ulockmgr_server - -rwsr-xr-x 1 root root 30108 Jan 9 2019 umount - -rwxr-xr-x 1 root root 34532 Feb 28 2019 uname - -rwxr-xr-x 2 root root 2345 Jan 5 2019 uncompress - -rwxr-xr-x 1 root root 149736 Feb 28 2019 vdir - -rwxr-xr-x 1 root root 34208 Jan 9 2019 wdctl - -rwxr-xr-x 1 root root 946 Jan 21 2019 which - lrwxrwxrwx 1 root root 8 Sep 26 2018 ypdomainname -> hostname - -rwxr-xr-x 1 root root 1983 Jan 5 2019 zcat - -rwxr-xr-x 1 root root 1677 Jan 5 2019 zcmp - -rwxr-xr-x 1 root root 5879 Jan 5 2019 zdiff - -rwxr-xr-x 1 root root 29 Jan 5 2019 zegrep - -rwxr-xr-x 1 root root 29 Jan 5 2019 zfgrep - -rwxr-xr-x 1 root root 2080 Jan 5 2019 zforce - -rwxr-xr-x 1 root root 7584 Jan 5 2019 zgrep - -rwxr-xr-x 1 root root 2205 Jan 5 2019 zless - -rwxr-xr-x 1 root root 1841 Jan 5 2019 zmore - -rwxr-xr-x 1 root root 4552 Jan 5 2019 znew -I: user script /srv/workspace/pbuilder/5314/tmp/hooks/D02_print_environment finished + -rwxr-xr-x 1 root root 1302248 Apr 18 2019 bash + -rwxr-xr-x 3 root root 38280 Jul 11 2019 bunzip2 + -rwxr-xr-x 3 root root 38280 Jul 11 2019 bzcat + lrwxrwxrwx 1 root root 6 Jul 11 2019 bzcmp -> bzdiff + -rwxr-xr-x 1 root root 2227 Jul 11 2019 bzdiff + lrwxrwxrwx 1 root root 6 Jul 11 2019 bzegrep -> bzgrep + -rwxr-xr-x 1 root root 4877 Jun 25 2019 bzexe + lrwxrwxrwx 1 root root 6 Jul 11 2019 bzfgrep -> bzgrep + -rwxr-xr-x 1 root root 3641 Jul 11 2019 bzgrep + -rwxr-xr-x 3 root root 38280 Jul 11 2019 bzip2 + -rwxr-xr-x 1 root root 17768 Jul 11 2019 bzip2recover + lrwxrwxrwx 1 root root 6 Jul 11 2019 bzless -> bzmore + -rwxr-xr-x 1 root root 1297 Jul 11 2019 bzmore + -rwxr-xr-x 1 root root 38692 Mar 1 2019 cat + -rwxr-xr-x 1 root root 75588 Mar 1 2019 chgrp + -rwxr-xr-x 1 root root 63268 Mar 1 2019 chmod + -rwxr-xr-x 1 root root 75588 Mar 1 2019 chown + -rwxr-xr-x 1 root root 153732 Mar 1 2019 cp + -rwxr-xr-x 1 root root 132820 Jan 18 2019 dash + -rwxr-xr-x 1 root root 120676 Mar 1 2019 date + -rwxr-xr-x 1 root root 92040 Mar 1 2019 dd + -rwxr-xr-x 1 root root 100620 Mar 1 2019 df + -rwxr-xr-x 1 root root 149736 Mar 1 2019 dir + -rwxr-xr-x 1 root root 79412 Jan 10 2019 dmesg + lrwxrwxrwx 1 root root 8 Sep 27 2018 dnsdomainname -> hostname + lrwxrwxrwx 1 root root 8 Sep 27 2018 domainname -> hostname + -rwxr-xr-x 1 root root 34532 Mar 1 2019 echo + -rwxr-xr-x 1 root root 28 Jan 8 2019 egrep + -rwxr-xr-x 1 root root 34532 Mar 1 2019 false + -rwxr-xr-x 1 root root 28 Jan 8 2019 fgrep + -rwxr-xr-x 1 root root 67700 Jan 10 2019 findmnt + -rwsr-xr-x 1 root root 30112 Apr 23 09:38 fusermount + -rwxr-xr-x 1 root root 206392 Jan 8 2019 grep + -rwxr-xr-x 2 root root 2345 Jan 6 2019 gunzip + -rwxr-xr-x 1 root root 6375 Jan 6 2019 gzexe + -rwxr-xr-x 1 root root 100952 Jan 6 2019 gzip + -rwxr-xr-x 1 root root 21916 Sep 27 2018 hostname + -rwxr-xr-x 1 root root 79752 Mar 1 2019 ln + -rwxr-xr-x 1 root root 55400 Jul 27 2018 login + -rwxr-xr-x 1 root root 149736 Mar 1 2019 ls + -rwxr-xr-x 1 root root 112032 Jan 10 2019 lsblk + -rwxr-xr-x 1 root root 87972 Mar 1 2019 mkdir + -rwxr-xr-x 1 root root 79748 Mar 1 2019 mknod + -rwxr-xr-x 1 root root 46916 Mar 1 2019 mktemp + -rwxr-xr-x 1 root root 42348 Jan 10 2019 more + -rwsr-xr-x 1 root root 50592 Jan 10 2019 mount + -rwxr-xr-x 1 root root 13724 Jan 10 2019 mountpoint + -rwxr-xr-x 1 root root 157832 Mar 1 2019 mv + lrwxrwxrwx 1 root root 8 Sep 27 2018 nisdomainname -> hostname + lrwxrwxrwx 1 root root 14 Feb 15 2019 pidof -> /sbin/killall5 + -rwxr-xr-x 1 root root 38660 Mar 1 2019 pwd + lrwxrwxrwx 1 root root 4 Apr 18 2019 rbash -> bash + -rwxr-xr-x 1 root root 46852 Mar 1 2019 readlink + -rwxr-xr-x 1 root root 75588 Mar 1 2019 rm + -rwxr-xr-x 1 root root 42756 Mar 1 2019 rmdir + -rwxr-xr-x 1 root root 22276 Jan 22 2019 run-parts + -rwxr-xr-x 1 root root 125036 Dec 23 2018 sed + lrwxrwxrwx 1 root root 4 Sep 23 09:28 sh -> bash + lrwxrwxrwx 1 root root 4 Sep 21 22:25 sh.distrib -> dash + -rwxr-xr-x 1 root root 34532 Mar 1 2019 sleep + -rwxr-xr-x 1 root root 79652 Mar 1 2019 stty + -rwsr-xr-x 1 root root 71072 Jan 10 2019 su + -rwxr-xr-x 1 root root 34564 Mar 1 2019 sync + -rwxr-xr-x 1 root root 504024 Apr 24 2019 tar + -rwxr-xr-x 1 root root 13860 Jan 22 2019 tempfile + -rwxr-xr-x 1 root root 104292 Mar 1 2019 touch + -rwxr-xr-x 1 root root 34532 Mar 1 2019 true + -rwxr-xr-x 1 root root 17768 Apr 23 09:38 ulockmgr_server + -rwsr-xr-x 1 root root 30108 Jan 10 2019 umount + -rwxr-xr-x 1 root root 34532 Mar 1 2019 uname + -rwxr-xr-x 2 root root 2345 Jan 6 2019 uncompress + -rwxr-xr-x 1 root root 149736 Mar 1 2019 vdir + -rwxr-xr-x 1 root root 34208 Jan 10 2019 wdctl + -rwxr-xr-x 1 root root 946 Jan 22 2019 which + lrwxrwxrwx 1 root root 8 Sep 27 2018 ypdomainname -> hostname + -rwxr-xr-x 1 root root 1983 Jan 6 2019 zcat + -rwxr-xr-x 1 root root 1677 Jan 6 2019 zcmp + -rwxr-xr-x 1 root root 5879 Jan 6 2019 zdiff + -rwxr-xr-x 1 root root 29 Jan 6 2019 zegrep + -rwxr-xr-x 1 root root 29 Jan 6 2019 zfgrep + -rwxr-xr-x 1 root root 2080 Jan 6 2019 zforce + -rwxr-xr-x 1 root root 7584 Jan 6 2019 zgrep + -rwxr-xr-x 1 root root 2205 Jan 6 2019 zless + -rwxr-xr-x 1 root root 1841 Jan 6 2019 zmore + -rwxr-xr-x 1 root root 4552 Jan 6 2019 znew +I: user script /srv/workspace/pbuilder/22984/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -437,7 +471,7 @@ Get: 226 http://deb.debian.org/debian buster/main i386 xdg-utils all 1.1.3-1+deb10u1 [73.7 kB] Get: 227 http://deb.debian.org/debian buster/main i386 texlive-base all 2018.20190227-2 [19.7 MB] Get: 228 http://deb.debian.org/debian buster/main i386 texlive-latex-base all 2018.20190227-2 [984 kB] -Fetched 167 MB in 3s (49.7 MB/s) +Fetched 167 MB in 59s (2832 kB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package install-info. (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 19234 files and directories currently installed.) @@ -1421,7 +1455,7 @@ fakeroot is already the newest version (1.23-1). 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. I: Building the package -I: Running cd /build/hol88-2.02.19940316/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-buildpackage -us -uc -b +I: Running cd /build/hol88-2.02.19940316/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path" HOME="/nonexistent/second-build" dpkg-buildpackage -us -uc -b dpkg-buildpackage: info: source package hol88 dpkg-buildpackage: info: source version 2.02.19940316-35 dpkg-buildpackage: info: source distribution unstable @@ -1675,39 +1709,24 @@ make[2]: Leaving directory '/build/hol88-2.02.19940316/Manual/Covers' make[1]: Leaving directory '/build/hol88-2.02.19940316/Manual' [ ! -f Makefile ] || for i in $(find Library -name Manual); do /usr/bin/make -C $i clean ; done -make[1]: Entering directory '/build/hol88-2.02.19940316/Library/pair/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex theorems.tex; \ -printf '\\begin{theindex}' >index.tex; \ -printf '\\mbox{}' >>index.tex; \ -printf '\\end{theindex}' >>index.tex -make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/pair/Manual' -make[1]: Entering directory '/build/hol88-2.02.19940316/Library/string/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/string/Manual' -make[1]: Entering directory '/build/hol88-2.02.19940316/Library/window/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex *.bak; \ -printf '\\begin{theindex}' >index.tex; \ -printf '\\mbox{}' >>index.tex; \ -printf '\\end{theindex}' >>index.tex -make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/window/Manual' -make[1]: Entering directory '/build/hol88-2.02.19940316/Library/pred_sets/Manual' +make[1]: Entering directory '/build/hol88-2.02.19940316/Library/taut/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/pred_sets/Manual' -make[1]: Entering directory '/build/hol88-2.02.19940316/Library/res_quan/Manual' +make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/taut/Manual' +make[1]: Entering directory '/build/hol88-2.02.19940316/Library/prettyp/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/res_quan/Manual' -make[1]: Entering directory '/build/hol88-2.02.19940316/Library/sets/Manual' +make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/prettyp/Manual' +make[1]: Entering directory '/build/hol88-2.02.19940316/Library/string/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/sets/Manual' -make[1]: Entering directory '/build/hol88-2.02.19940316/Library/taut/Manual' +make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/string/Manual' +make[1]: Entering directory '/build/hol88-2.02.19940316/Library/trs/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/taut/Manual' -make[1]: Entering directory '/build/hol88-2.02.19940316/Library/finite_sets/Manual' +make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/trs/Manual' +make[1]: Entering directory '/build/hol88-2.02.19940316/Library/unwind/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/finite_sets/Manual' -make[1]: Entering directory '/build/hol88-2.02.19940316/Library/more_arithmetic/Manual' +make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/unwind/Manual' +make[1]: Entering directory '/build/hol88-2.02.19940316/Library/pred_sets/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/more_arithmetic/Manual' +make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/pred_sets/Manual' make[1]: Entering directory '/build/hol88-2.02.19940316/Library/abs_theory/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ @@ -1715,6 +1734,30 @@ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/abs_theory/Manual' +make[1]: Entering directory '/build/hol88-2.02.19940316/Library/sets/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/sets/Manual' +make[1]: Entering directory '/build/hol88-2.02.19940316/Library/window/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex *.bak; \ +printf '\\begin{theindex}' >index.tex; \ +printf '\\mbox{}' >>index.tex; \ +printf '\\end{theindex}' >>index.tex +make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/window/Manual' +make[1]: Entering directory '/build/hol88-2.02.19940316/Library/latex-hol/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/latex-hol/Manual' +make[1]: Entering directory '/build/hol88-2.02.19940316/Library/pair/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex theorems.tex; \ +printf '\\begin{theindex}' >index.tex; \ +printf '\\mbox{}' >>index.tex; \ +printf '\\end{theindex}' >>index.tex +make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/pair/Manual' +make[1]: Entering directory '/build/hol88-2.02.19940316/Library/record_proof/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/record_proof/Manual' +make[1]: Entering directory '/build/hol88-2.02.19940316/Library/arith/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/arith/Manual' make[1]: Entering directory '/build/hol88-2.02.19940316/Library/reals/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg; \ @@ -1722,9 +1765,9 @@ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/reals/Manual' -make[1]: Entering directory '/build/hol88-2.02.19940316/Library/arith/Manual' +make[1]: Entering directory '/build/hol88-2.02.19940316/Library/finite_sets/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/arith/Manual' +make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/finite_sets/Manual' make[1]: Entering directory '/build/hol88-2.02.19940316/Library/wellorder/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ @@ -1732,15 +1775,12 @@ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/wellorder/Manual' -make[1]: Entering directory '/build/hol88-2.02.19940316/Library/unwind/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/unwind/Manual' -make[1]: Entering directory '/build/hol88-2.02.19940316/Library/record_proof/Manual' +make[1]: Entering directory '/build/hol88-2.02.19940316/Library/more_arithmetic/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/record_proof/Manual' -make[1]: Entering directory '/build/hol88-2.02.19940316/Library/prettyp/Manual' +make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/more_arithmetic/Manual' +make[1]: Entering directory '/build/hol88-2.02.19940316/Library/word/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/prettyp/Manual' +make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/word/Manual' make[1]: Entering directory '/build/hol88-2.02.19940316/Library/parser/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/parser/Manual' @@ -1751,15 +1791,9 @@ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/reduce/Manual' -make[1]: Entering directory '/build/hol88-2.02.19940316/Library/trs/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/trs/Manual' -make[1]: Entering directory '/build/hol88-2.02.19940316/Library/word/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/word/Manual' -make[1]: Entering directory '/build/hol88-2.02.19940316/Library/latex-hol/Manual' +make[1]: Entering directory '/build/hol88-2.02.19940316/Library/res_quan/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/latex-hol/Manual' +make[1]: Leaving directory '/build/hol88-2.02.19940316/Library/res_quan/Manual' make[1]: Entering directory '/build/hol88-2.02.19940316/Library/numeral/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ @@ -1813,7 +1847,7 @@ >PATH=$(pwd):$PATH /usr/bin/make all make[1]: Entering directory '/build/hol88-2.02.19940316' date -Mon Oct 25 13:36:50 -12 2021 +Wed Sep 23 09:33:09 +14 2020 /usr/bin/make hol make[2]: Entering directory '/build/hol88-2.02.19940316' if [ cl = cl ]; then\ @@ -2925,53 +2959,53 @@ ;; Loading "lisp/f-typeml" start address -T 0x7e37e8 ;; Finished loading "lisp/f-typeml" ;; Loading "lisp/f-dml" -start address -T 0x7f0a00 ;; Finished loading "lisp/f-dml" +start address -T 0x7f0a28 ;; Finished loading "lisp/f-dml" ;; Loading "lisp/f-format" -start address -T 0x7f6448 ;; Finished loading "lisp/f-format" +start address -T 0x7f6470 ;; Finished loading "lisp/f-format" ;; Loading "lisp/f-tran" -start address -T 0x7fab88 ;; Finished loading "lisp/f-tran" +start address -T 0x7fabb0 ;; Finished loading "lisp/f-tran" ;; Loading "lisp/f-iox-stand" -start address -T 0x8079c0 ;; Finished loading "lisp/f-iox-stand" +start address -T 0x8079e8 ;; Finished loading "lisp/f-iox-stand" ;; Loading "lisp/f-writml" -start address -T 0x80c370 ;; Finished loading "lisp/f-writml" +start address -T 0x80c398 ;; Finished loading "lisp/f-writml" ;; Loading "lisp/f-tml" -start address -T 0x810948 ;; Finished loading "lisp/f-tml" +start address -T 0x810970 ;; Finished loading "lisp/f-tml" ;; Loading "lisp/f-lis" -start address -T 0x81c1a0 ;; Finished loading "lisp/f-lis" +start address -T 0x81c1c8 ;; Finished loading "lisp/f-lis" ;; Loading "lisp/f-ol-rec" -start address -T 0x81f4a0 ;; Finished loading "lisp/f-ol-rec" +start address -T 0x81f4c8 ;; Finished loading "lisp/f-ol-rec" ;; Loading "lisp/f-help" -start address -T 0x822a50 ;; Finished loading "lisp/f-help" +start address -T 0x822a78 ;; Finished loading "lisp/f-help" start address -T 0x667590 ;; Finished loading "lisp/mk-ml" 599 >;; Loading "lisp/mk-hol-lcf" ;; Loading "lisp/f-parsol" -start address -T 0x827588 ;; Finished loading "lisp/f-parsol" +start address -T 0x8275b0 ;; Finished loading "lisp/f-parsol" ;; Loading "lisp/f-typeol" -start address -T 0x82c980 ;; Finished loading "lisp/f-typeol" +start address -T 0x82c9a8 ;; Finished loading "lisp/f-typeol" ;; Loading "lisp/f-help" -start address -T 0x831958 ;; Finished loading "lisp/f-help" +start address -T 0x831980 ;; Finished loading "lisp/f-help" ;; Loading "lisp/f-format" -start address -T 0x8340b8 ;; Finished loading "lisp/f-format" +start address -T 0x8340e0 ;; Finished loading "lisp/f-format" ;; Loading "lisp/f-writol" -start address -T 0x8387f8 ;; Finished loading "lisp/f-writol" +start address -T 0x838820 ;; Finished loading "lisp/f-writol" ;; Loading "lisp/f-thyfns" -start address -T 0x83efc8 ;; Finished loading "lisp/f-thyfns" +start address -T 0x83eff0 ;; Finished loading "lisp/f-thyfns" ;; Loading "lisp/f-freadth" Warning: lisp/f-freadth.l is redefining function THY-READ -start address -T 0x84c538 ;; Finished loading "lisp/f-freadth" +start address -T 0x84c560 ;; Finished loading "lisp/f-freadth" ;; Loading "lisp/f-ol-syntax" -start address -T 0x850230 ;; Finished loading "lisp/f-ol-syntax" +start address -T 0x850258 ;; Finished loading "lisp/f-ol-syntax" ;; Loading "lisp/f-subst" -start address -T 0x859a68 ;; Finished loading "lisp/f-subst" +start address -T 0x859a90 ;; Finished loading "lisp/f-subst" ;; Loading "lisp/f-inst" -start address -T 0x85fdd8 ;; Finished loading "lisp/f-inst" +start address -T 0x85fe00 ;; Finished loading "lisp/f-inst" ;; Loading "lisp/f-simpl" -start address -T 0x865ce0 ;; Finished loading "lisp/f-simpl" +start address -T 0x865d08 ;; Finished loading "lisp/f-simpl" ;; Loading "lisp/f-ol-net" -start address -T 0x8694c8 ;; Finished loading "lisp/f-ol-net" -start address -T 0x8251b0 ;; Finished loading "lisp/mk-hol-lcf" +start address -T 0x8694f0 ;; Finished loading "lisp/f-ol-net" +start address -T 0x8251d8 ;; Finished loading "lisp/mk-hol-lcf" 599 > @@ -2987,7 +3021,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 25/10/21 +HOL-LCF version 2.02 (GCL) created 23/9/20 # mem = - : (* -> * list -> bool) @@ -3063,53 +3097,53 @@ ;; Loading "lisp/f-typeml" start address -T 0x7e37e8 ;; Finished loading "lisp/f-typeml" ;; Loading "lisp/f-dml" -start address -T 0x7f0a00 ;; Finished loading "lisp/f-dml" +start address -T 0x7f0a28 ;; Finished loading "lisp/f-dml" ;; Loading "lisp/f-format" -start address -T 0x7f6448 ;; Finished loading "lisp/f-format" +start address -T 0x7f6470 ;; Finished loading "lisp/f-format" ;; Loading "lisp/f-tran" -start address -T 0x7fab88 ;; Finished loading "lisp/f-tran" +start address -T 0x7fabb0 ;; Finished loading "lisp/f-tran" ;; Loading "lisp/f-iox-stand" -start address -T 0x8079c0 ;; Finished loading "lisp/f-iox-stand" +start address -T 0x8079e8 ;; Finished loading "lisp/f-iox-stand" ;; Loading "lisp/f-writml" -start address -T 0x80c370 ;; Finished loading "lisp/f-writml" +start address -T 0x80c398 ;; Finished loading "lisp/f-writml" ;; Loading "lisp/f-tml" -start address -T 0x810948 ;; Finished loading "lisp/f-tml" +start address -T 0x810970 ;; Finished loading "lisp/f-tml" ;; Loading "lisp/f-lis" -start address -T 0x81c1a0 ;; Finished loading "lisp/f-lis" +start address -T 0x81c1c8 ;; Finished loading "lisp/f-lis" ;; Loading "lisp/f-ol-rec" -start address -T 0x81f4a0 ;; Finished loading "lisp/f-ol-rec" +start address -T 0x81f4c8 ;; Finished loading "lisp/f-ol-rec" ;; Loading "lisp/f-help" -start address -T 0x822a50 ;; Finished loading "lisp/f-help" +start address -T 0x822a78 ;; Finished loading "lisp/f-help" start address -T 0x667590 ;; Finished loading "lisp/mk-ml" 599 >;; Loading "lisp/mk-hol-lcf" ;; Loading "lisp/f-parsol" -start address -T 0x827588 ;; Finished loading "lisp/f-parsol" +start address -T 0x8275b0 ;; Finished loading "lisp/f-parsol" ;; Loading "lisp/f-typeol" -start address -T 0x82c980 ;; Finished loading "lisp/f-typeol" +start address -T 0x82c9a8 ;; Finished loading "lisp/f-typeol" ;; Loading "lisp/f-help" -start address -T 0x831958 ;; Finished loading "lisp/f-help" +start address -T 0x831980 ;; Finished loading "lisp/f-help" ;; Loading "lisp/f-format" -start address -T 0x8340b8 ;; Finished loading "lisp/f-format" +start address -T 0x8340e0 ;; Finished loading "lisp/f-format" ;; Loading "lisp/f-writol" -start address -T 0x8387f8 ;; Finished loading "lisp/f-writol" +start address -T 0x838820 ;; Finished loading "lisp/f-writol" ;; Loading "lisp/f-thyfns" -start address -T 0x83efc8 ;; Finished loading "lisp/f-thyfns" +start address -T 0x83eff0 ;; Finished loading "lisp/f-thyfns" ;; Loading "lisp/f-freadth" Warning: lisp/f-freadth.l is redefining function THY-READ -start address -T 0x84c538 ;; Finished loading "lisp/f-freadth" +start address -T 0x84c560 ;; Finished loading "lisp/f-freadth" ;; Loading "lisp/f-ol-syntax" -start address -T 0x850230 ;; Finished loading "lisp/f-ol-syntax" +start address -T 0x850258 ;; Finished loading "lisp/f-ol-syntax" ;; Loading "lisp/f-subst" -start address -T 0x859a68 ;; Finished loading "lisp/f-subst" +start address -T 0x859a90 ;; Finished loading "lisp/f-subst" ;; Loading "lisp/f-inst" -start address -T 0x85fdd8 ;; Finished loading "lisp/f-inst" +start address -T 0x85fe00 ;; Finished loading "lisp/f-inst" ;; Loading "lisp/f-simpl" -start address -T 0x865ce0 ;; Finished loading "lisp/f-simpl" +start address -T 0x865d08 ;; Finished loading "lisp/f-simpl" ;; Loading "lisp/f-ol-net" -start address -T 0x8694c8 ;; Finished loading "lisp/f-ol-net" -start address -T 0x8251b0 ;; Finished loading "lisp/mk-hol-lcf" +start address -T 0x8694f0 ;; Finished loading "lisp/f-ol-net" +start address -T 0x8251d8 ;; Finished loading "lisp/mk-hol-lcf" 599 > @@ -3125,7 +3159,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 25/10/21 +HOL-LCF version 2.02 (GCL) created 23/9/20 #.............start address -T 0x94c008 () : void @@ -3222,53 +3256,53 @@ ;; Loading "lisp/f-typeml" start address -T 0x7e37e8 ;; Finished loading "lisp/f-typeml" ;; Loading "lisp/f-dml" -start address -T 0x7f0a00 ;; Finished loading "lisp/f-dml" +start address -T 0x7f0a28 ;; Finished loading "lisp/f-dml" ;; Loading "lisp/f-format" -start address -T 0x7f6448 ;; Finished loading "lisp/f-format" +start address -T 0x7f6470 ;; Finished loading "lisp/f-format" ;; Loading "lisp/f-tran" -start address -T 0x7fab88 ;; Finished loading "lisp/f-tran" +start address -T 0x7fabb0 ;; Finished loading "lisp/f-tran" ;; Loading "lisp/f-iox-stand" -start address -T 0x8079c0 ;; Finished loading "lisp/f-iox-stand" +start address -T 0x8079e8 ;; Finished loading "lisp/f-iox-stand" ;; Loading "lisp/f-writml" -start address -T 0x80c370 ;; Finished loading "lisp/f-writml" +start address -T 0x80c398 ;; Finished loading "lisp/f-writml" ;; Loading "lisp/f-tml" -start address -T 0x810948 ;; Finished loading "lisp/f-tml" +start address -T 0x810970 ;; Finished loading "lisp/f-tml" ;; Loading "lisp/f-lis" -start address -T 0x81c1a0 ;; Finished loading "lisp/f-lis" +start address -T 0x81c1c8 ;; Finished loading "lisp/f-lis" ;; Loading "lisp/f-ol-rec" -start address -T 0x81f4a0 ;; Finished loading "lisp/f-ol-rec" +start address -T 0x81f4c8 ;; Finished loading "lisp/f-ol-rec" ;; Loading "lisp/f-help" -start address -T 0x822a50 ;; Finished loading "lisp/f-help" +start address -T 0x822a78 ;; Finished loading "lisp/f-help" start address -T 0x667590 ;; Finished loading "lisp/mk-ml" 599 >;; Loading "lisp/mk-hol-lcf" ;; Loading "lisp/f-parsol" -start address -T 0x827588 ;; Finished loading "lisp/f-parsol" +start address -T 0x8275b0 ;; Finished loading "lisp/f-parsol" ;; Loading "lisp/f-typeol" -start address -T 0x82c980 ;; Finished loading "lisp/f-typeol" +start address -T 0x82c9a8 ;; Finished loading "lisp/f-typeol" ;; Loading "lisp/f-help" -start address -T 0x831958 ;; Finished loading "lisp/f-help" +start address -T 0x831980 ;; Finished loading "lisp/f-help" ;; Loading "lisp/f-format" -start address -T 0x8340b8 ;; Finished loading "lisp/f-format" +start address -T 0x8340e0 ;; Finished loading "lisp/f-format" ;; Loading "lisp/f-writol" -start address -T 0x8387f8 ;; Finished loading "lisp/f-writol" +start address -T 0x838820 ;; Finished loading "lisp/f-writol" ;; Loading "lisp/f-thyfns" -start address -T 0x83efc8 ;; Finished loading "lisp/f-thyfns" +start address -T 0x83eff0 ;; Finished loading "lisp/f-thyfns" ;; Loading "lisp/f-freadth" Warning: lisp/f-freadth.l is redefining function THY-READ -start address -T 0x84c538 ;; Finished loading "lisp/f-freadth" +start address -T 0x84c560 ;; Finished loading "lisp/f-freadth" ;; Loading "lisp/f-ol-syntax" -start address -T 0x850230 ;; Finished loading "lisp/f-ol-syntax" +start address -T 0x850258 ;; Finished loading "lisp/f-ol-syntax" ;; Loading "lisp/f-subst" -start address -T 0x859a68 ;; Finished loading "lisp/f-subst" +start address -T 0x859a90 ;; Finished loading "lisp/f-subst" ;; Loading "lisp/f-inst" -start address -T 0x85fdd8 ;; Finished loading "lisp/f-inst" +start address -T 0x85fe00 ;; Finished loading "lisp/f-inst" ;; Loading "lisp/f-simpl" -start address -T 0x865ce0 ;; Finished loading "lisp/f-simpl" +start address -T 0x865d08 ;; Finished loading "lisp/f-simpl" ;; Loading "lisp/f-ol-net" -start address -T 0x8694c8 ;; Finished loading "lisp/f-ol-net" -start address -T 0x8251b0 ;; Finished loading "lisp/mk-hol-lcf" +start address -T 0x8694f0 ;; Finished loading "lisp/f-ol-net" +start address -T 0x8251d8 ;; Finished loading "lisp/mk-hol-lcf" 599 > @@ -3284,7 +3318,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 25/10/21 +HOL-LCF version 2.02 (GCL) created 23/9/20 #.............start address -T 0x94c008 () : void @@ -3414,53 +3448,53 @@ ;; Loading "lisp/f-typeml" start address -T 0x7e37e8 ;; Finished loading "lisp/f-typeml" ;; Loading "lisp/f-dml" -start address -T 0x7f0a00 ;; Finished loading "lisp/f-dml" +start address -T 0x7f0a28 ;; Finished loading "lisp/f-dml" ;; Loading "lisp/f-format" -start address -T 0x7f6448 ;; Finished loading "lisp/f-format" +start address -T 0x7f6470 ;; Finished loading "lisp/f-format" ;; Loading "lisp/f-tran" -start address -T 0x7fab88 ;; Finished loading "lisp/f-tran" +start address -T 0x7fabb0 ;; Finished loading "lisp/f-tran" ;; Loading "lisp/f-iox-stand" -start address -T 0x8079c0 ;; Finished loading "lisp/f-iox-stand" +start address -T 0x8079e8 ;; Finished loading "lisp/f-iox-stand" ;; Loading "lisp/f-writml" -start address -T 0x80c370 ;; Finished loading "lisp/f-writml" +start address -T 0x80c398 ;; Finished loading "lisp/f-writml" ;; Loading "lisp/f-tml" -start address -T 0x810948 ;; Finished loading "lisp/f-tml" +start address -T 0x810970 ;; Finished loading "lisp/f-tml" ;; Loading "lisp/f-lis" -start address -T 0x81c1a0 ;; Finished loading "lisp/f-lis" +start address -T 0x81c1c8 ;; Finished loading "lisp/f-lis" ;; Loading "lisp/f-ol-rec" -start address -T 0x81f4a0 ;; Finished loading "lisp/f-ol-rec" +start address -T 0x81f4c8 ;; Finished loading "lisp/f-ol-rec" ;; Loading "lisp/f-help" -start address -T 0x822a50 ;; Finished loading "lisp/f-help" +start address -T 0x822a78 ;; Finished loading "lisp/f-help" start address -T 0x667590 ;; Finished loading "lisp/mk-ml" 599 >;; Loading "lisp/mk-hol-lcf" ;; Loading "lisp/f-parsol" -start address -T 0x827588 ;; Finished loading "lisp/f-parsol" +start address -T 0x8275b0 ;; Finished loading "lisp/f-parsol" ;; Loading "lisp/f-typeol" -start address -T 0x82c980 ;; Finished loading "lisp/f-typeol" +start address -T 0x82c9a8 ;; Finished loading "lisp/f-typeol" ;; Loading "lisp/f-help" -start address -T 0x831958 ;; Finished loading "lisp/f-help" +start address -T 0x831980 ;; Finished loading "lisp/f-help" ;; Loading "lisp/f-format" -start address -T 0x8340b8 ;; Finished loading "lisp/f-format" +start address -T 0x8340e0 ;; Finished loading "lisp/f-format" ;; Loading "lisp/f-writol" -start address -T 0x8387f8 ;; Finished loading "lisp/f-writol" +start address -T 0x838820 ;; Finished loading "lisp/f-writol" ;; Loading "lisp/f-thyfns" -start address -T 0x83efc8 ;; Finished loading "lisp/f-thyfns" +start address -T 0x83eff0 ;; Finished loading "lisp/f-thyfns" ;; Loading "lisp/f-freadth" Warning: lisp/f-freadth.l is redefining function THY-READ -start address -T 0x84c538 ;; Finished loading "lisp/f-freadth" +start address -T 0x84c560 ;; Finished loading "lisp/f-freadth" ;; Loading "lisp/f-ol-syntax" -start address -T 0x850230 ;; Finished loading "lisp/f-ol-syntax" +start address -T 0x850258 ;; Finished loading "lisp/f-ol-syntax" ;; Loading "lisp/f-subst" -start address -T 0x859a68 ;; Finished loading "lisp/f-subst" +start address -T 0x859a90 ;; Finished loading "lisp/f-subst" ;; Loading "lisp/f-inst" -start address -T 0x85fdd8 ;; Finished loading "lisp/f-inst" +start address -T 0x85fe00 ;; Finished loading "lisp/f-inst" ;; Loading "lisp/f-simpl" -start address -T 0x865ce0 ;; Finished loading "lisp/f-simpl" +start address -T 0x865d08 ;; Finished loading "lisp/f-simpl" ;; Loading "lisp/f-ol-net" -start address -T 0x8694c8 ;; Finished loading "lisp/f-ol-net" -start address -T 0x8251b0 ;; Finished loading "lisp/mk-hol-lcf" +start address -T 0x8694f0 ;; Finished loading "lisp/f-ol-net" +start address -T 0x8251d8 ;; Finished loading "lisp/mk-hol-lcf" 599 > @@ -3476,7 +3510,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 25/10/21 +HOL-LCF version 2.02 (GCL) created 23/9/20 # concat = - : (string -> string -> string) @@ -3582,7 +3616,7 @@ start address -T 0x86b640 ;; Finished loading "lisp/f-ol-net" start address -T 0x827328 ;; Finished loading "lisp/mk-hol-lcf" - version 2.02 (GCL) created 25/10/21 + version 2.02 (GCL) created 23/9/20 #...start address -T 0x86f4a8 () : void @@ -3895,7 +3929,7 @@ /build/hol88-2.02.19940316/hol-lcf < /build/hol88-2.02.19940316/theories/mk_PPLAMB.ml;\ cd /build/hol88-2.02.19940316 -HOL-LCF version 2.02 (GCL) created 25/10/21 +HOL-LCF version 2.02 (GCL) created 23/9/20 ###########################() : void @@ -3908,7 +3942,7 @@ /build/hol88-2.02.19940316/hol-lcf < /build/hol88-2.02.19940316/theories/mk_bool.ml;\ cd /build/hol88-2.02.19940316 -HOL-LCF version 2.02 (GCL) created 25/10/21 +HOL-LCF version 2.02 (GCL) created 23/9/20 ################################################################################################() : void @@ -4053,7 +4087,7 @@ /build/hol88-2.02.19940316/hol-lcf < /build/hol88-2.02.19940316/theories/mk_ind.ml;\ cd /build/hol88-2.02.19940316 -HOL-LCF version 2.02 (GCL) created 25/10/21 +HOL-LCF version 2.02 (GCL) created 23/9/20 ############################() : void @@ -4096,7 +4130,7 @@ /build/hol88-2.02.19940316/hol-lcf < /build/hol88-2.02.19940316/theories/mk_BASIC-HOL.ml;\ cd /build/hol88-2.02.19940316 -HOL-LCF version 2.02 (GCL) created 25/10/21 +HOL-LCF version 2.02 (GCL) created 23/9/20 ############################Theory ind loaded () : void @@ -4133,7 +4167,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/10/21 +HOL-LCF version 2.02 (GCL) created 23/9/20 # map2 = - : (((* # **) -> ***) -> (* list # ** list) -> *** list) @@ -4174,7 +4208,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/10/21 +HOL-LCF version 2.02 (GCL) created 23/9/20 #() : void @@ -4576,7 +4610,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/10/21 +HOL-LCF version 2.02 (GCL) created 23/9/20 #() : void @@ -4644,7 +4678,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/10/21 +HOL-LCF version 2.02 (GCL) created 23/9/20 #() : void @@ -4849,7 +4883,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/10/21 +HOL-LCF version 2.02 (GCL) created 23/9/20 #() : void @@ -4973,7 +5007,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/10/21 +HOL-LCF version 2.02 (GCL) created 23/9/20 #() : void @@ -5059,7 +5093,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/10/21 +HOL-LCF version 2.02 (GCL) created 23/9/20 #() : void @@ -5152,7 +5186,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/10/21 +HOL-LCF version 2.02 (GCL) created 23/9/20 #() : void @@ -5221,7 +5255,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/10/21 +HOL-LCF version 2.02 (GCL) created 23/9/20 #() : void @@ -5326,7 +5360,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/10/21 +HOL-LCF version 2.02 (GCL) created 23/9/20 #() : void @@ -5561,7 +5595,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/10/21 +HOL-LCF version 2.02 (GCL) created 23/9/20 #() : void @@ -5587,7 +5621,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/10/21 +HOL-LCF version 2.02 (GCL) created 23/9/20 #() : void @@ -5715,7 +5749,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/10/21 +HOL-LCF version 2.02 (GCL) created 23/9/20 #() : void @@ -5763,7 +5797,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/10/21 +HOL-LCF version 2.02 (GCL) created 23/9/20 #() : void @@ -5830,7 +5864,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/10/21 +HOL-LCF version 2.02 (GCL) created 23/9/20 #() : void @@ -5889,7 +5923,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/10/21 +HOL-LCF version 2.02 (GCL) created 23/9/20 #() : void @@ -5945,7 +5979,7 @@ 'lisp `(setup)`;;' >foo1 echo 'lisp `(throw (quote eof) t)`;; #+native-reloc(progn (with-open-file (s "foo1") (let ((*standard-input* s)) (tml)))(ml-save "basic-hol")) #-native-reloc(let ((si::*collect-binary-modules* t)(si::*binary-modules* (with-open-file (s "bm.l") (read s)))) (with-open-file (s "foo1") (let ((*standard-input* s)) (tml)))(compiler::link (remove-duplicates si::*binary-modules* :test (function equal)) "basic-hol" "(progn (load \"debian/gcl_patch.l\")(load \"foo\")(with-open-file (s \"foo1\") (let ((*standard-input* s)) (tml)))(ml-save \"basic-hol\")(quit))" "" nil)(with-open-file (s "bm.l" :direction :output) (prin1 si::*binary-modules* s))(quit))`;;' | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/10/21 +HOL-LCF version 2.02 (GCL) created 23/9/20 #GCL (GNU Common Lisp) 2.6.12 CLtL1 Fri Apr 22 15:51:11 UTC 2016 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -5958,7 +5992,7 @@ /tmp/ > -HOL-LCF version 2.02 (GCL) created 25/10/21 +HOL-LCF version 2.02 (GCL) created 23/9/20 #() : void @@ -6010,7 +6044,7 @@ /build/hol88-2.02.19940316/basic-hol < /build/hol88-2.02.19940316/theories/mk_combin.ml;\ cd /build/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 25/10/21 +BASIC-HOL version 2.02 (GCL) created 23/9/20 ##########################() : void @@ -6041,7 +6075,7 @@ /build/hol88-2.02.19940316/basic-hol < /build/hol88-2.02.19940316/theories/mk_num.ml;\ cd /build/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 25/10/21 +BASIC-HOL version 2.02 (GCL) created 23/9/20 ##############################() : void @@ -6128,7 +6162,7 @@ /build/hol88-2.02.19940316/basic-hol < /build/hol88-2.02.19940316/theories/mk_prim_rec.ml;\ cd /build/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 25/10/21 +BASIC-HOL version 2.02 (GCL) created 23/9/20 #######################################################################() : void @@ -6281,7 +6315,7 @@ /build/hol88-2.02.19940316/basic-hol < /build/hol88-2.02.19940316/theories/mk_fun.ml;\ cd /build/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 25/10/21 +BASIC-HOL version 2.02 (GCL) created 23/9/20 ###########################() : void @@ -6316,7 +6350,7 @@ /build/hol88-2.02.19940316/basic-hol < /build/hol88-2.02.19940316/theories/mk_arith_thms.ml;\ cd /build/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 25/10/21 +BASIC-HOL version 2.02 (GCL) created 23/9/20 #############################() : void @@ -6377,7 +6411,7 @@ #################() : void ## -BASIC-HOL version 2.02 (GCL) created 25/10/21 +BASIC-HOL version 2.02 (GCL) created 23/9/20 ###########################Theory arithmetic loaded () : void @@ -6872,7 +6906,7 @@ /build/hol88-2.02.19940316/basic-hol < /build/hol88-2.02.19940316/theories/mk_list_thms.ml;\ cd /build/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 25/10/21 +BASIC-HOL version 2.02 (GCL) created 23/9/20 ##################################() : void @@ -7019,7 +7053,7 @@ |- !x f. ?! fn. (fn[] = x) /\ (!h t. fn(CONS h t) = f(fn t)h t) ## -BASIC-HOL version 2.02 (GCL) created 25/10/21 +BASIC-HOL version 2.02 (GCL) created 23/9/20 #################################Theory list loaded () : void @@ -7358,7 +7392,7 @@ ##() : void ## -BASIC-HOL version 2.02 (GCL) created 25/10/21 +BASIC-HOL version 2.02 (GCL) created 23/9/20 ###############################Theory list loaded () : void @@ -8855,7 +8889,7 @@ /build/hol88-2.02.19940316/basic-hol < /build/hol88-2.02.19940316/theories/mk_tree.ml;\ cd /build/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 25/10/21 +BASIC-HOL version 2.02 (GCL) created 23/9/20 #############################() : void @@ -9239,7 +9273,7 @@ /build/hol88-2.02.19940316/basic-hol < /build/hol88-2.02.19940316/theories/mk_ltree.ml;\ cd /build/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 25/10/21 +BASIC-HOL version 2.02 (GCL) created 23/9/20 ############################() : void @@ -9537,7 +9571,7 @@ /build/hol88-2.02.19940316/basic-hol < /build/hol88-2.02.19940316/theories/mk_tydefs.ml;\ cd /build/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 25/10/21 +BASIC-HOL version 2.02 (GCL) created 23/9/20 ############################() : void @@ -9677,7 +9711,7 @@ /build/hol88-2.02.19940316/basic-hol < /build/hol88-2.02.19940316/theories/mk_sum.ml;\ cd /build/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 25/10/21 +BASIC-HOL version 2.02 (GCL) created 23/9/20 ############################################() : void @@ -9774,7 +9808,7 @@ /build/hol88-2.02.19940316/basic-hol < /build/hol88-2.02.19940316/theories/mk_one.ml;\ cd /build/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 25/10/21 +BASIC-HOL version 2.02 (GCL) created 23/9/20 ##################################() : void @@ -9804,7 +9838,7 @@ | /build/hol88-2.02.19940316/basic-hol;\ cd /build/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 25/10/21 +BASIC-HOL version 2.02 (GCL) created 23/9/20 #() : void @@ -9821,7 +9855,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 25/10/21 +BASIC-HOL version 2.02 (GCL) created 23/9/20 #Theory num loaded () : void @@ -9840,7 +9874,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 25/10/21 +BASIC-HOL version 2.02 (GCL) created 23/9/20 #() : void @@ -9997,7 +10031,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 25/10/21 +BASIC-HOL version 2.02 (GCL) created 23/9/20 # @@ -10035,7 +10069,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 25/10/21 +BASIC-HOL version 2.02 (GCL) created 23/9/20 # @@ -10069,7 +10103,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 25/10/21 +BASIC-HOL version 2.02 (GCL) created 23/9/20 #() : void @@ -10154,7 +10188,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 25/10/21 +BASIC-HOL version 2.02 (GCL) created 23/9/20 #() : void @@ -10195,7 +10229,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 25/10/21 +BASIC-HOL version 2.02 (GCL) created 23/9/20 #() : void @@ -10379,7 +10413,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 25/10/21 +BASIC-HOL version 2.02 (GCL) created 23/9/20 # define_load_lib_function = - : (string list -> void -> void) @@ -10453,7 +10487,7 @@ 'lisp `(setup)`;;' >foo2 echo 'lisp `(throw (quote eof) t)`;; #+native-reloc(progn (with-open-file (s "foo2") (let ((*standard-input* s)) (tml)))(ml-save "hol")) #-native-reloc(let ((si::*collect-binary-modules* t)(si::*binary-modules* (with-open-file (s "bm.l") (read s)))) (with-open-file (s "foo2") (let ((*standard-input* s)) (tml)))(compiler::link (remove-duplicates si::*binary-modules* :test (function equal)) "hol" "(progn (load \"debian/gcl_patch.l\")(load \"foo\")(with-open-file (s \"foo1\") (let ((*standard-input* s)) (tml)))(with-open-file (s \"foo2\") (let ((*standard-input* s)) (tml)))(ml-save \"hol\")(quit))" "" nil)(quit))`;;' | basic-hol -BASIC-HOL version 2.02 (GCL) created 25/10/21 +BASIC-HOL version 2.02 (GCL) created 23/9/20 #GCL (GNU Common Lisp) 2.6.12 CLtL1 Fri Apr 22 15:51:11 UTC 2016 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -10466,7 +10500,7 @@ /tmp/ > -BASIC-HOL version 2.02 (GCL) created 25/10/21 +BASIC-HOL version 2.02 (GCL) created 23/9/20 #() : void @@ -10530,11 +10564,11 @@ =======> hol88 version 2.02 (GCL) made make[2]: Leaving directory '/build/hol88-2.02.19940316' date -Mon Oct 25 13:40:03 -12 2021 +Wed Sep 23 09:35:38 +14 2020 /usr/bin/make library make[2]: Entering directory '/build/hol88-2.02.19940316' date -Mon Oct 25 13:40:04 -12 2021 +Wed Sep 23 09:35:38 +14 2020 (cd /build/hol88-2.02.19940316/Library; /usr/bin/make LispType=cl\ Obj=o\ Lisp=gcl\ @@ -10557,7 +10591,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -10641,7 +10675,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -10747,7 +10781,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -11497,7 +11531,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -11520,7 +11554,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -11563,7 +11597,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -11599,7 +11633,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -11651,7 +11685,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -11683,7 +11717,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -11721,7 +11755,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -11749,7 +11783,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -11826,7 +11860,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -11848,7 +11882,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -11902,7 +11936,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -11951,7 +11985,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -12102,7 +12136,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -12146,7 +12180,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -12221,7 +12255,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -12271,7 +12305,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -12334,7 +12368,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -12387,7 +12421,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -12433,7 +12467,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -12521,7 +12555,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -12559,7 +12593,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -12620,7 +12654,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -12684,7 +12718,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -12710,7 +12744,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -12735,7 +12769,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -12774,7 +12808,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -12850,7 +12884,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -13587,7 +13621,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -13610,7 +13644,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -13653,7 +13687,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -13688,7 +13722,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -13729,7 +13763,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -13792,7 +13826,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -13815,7 +13849,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -13840,7 +13874,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -13867,7 +13901,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -13903,7 +13937,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -14435,7 +14469,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -14458,7 +14492,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -14492,7 +14526,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -14547,7 +14581,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -14638,7 +14672,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -14807,7 +14841,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -14994,7 +15028,7 @@ WOSET_TRANS_LE = |- !l. woset l ==> (!x y z. l(x,y) /\ less l(y,z) ==> less l(x,z)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 143 WOSET_WELL_CONTRAPOS = @@ -15040,7 +15074,7 @@ l(ms z,m) /\ l(ms z,n) ==> (f z = g z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1165 WO_RECURSE_LOCAL = @@ -15070,7 +15104,7 @@ (!f g x. (!y. less l(ms y,ms x) ==> (f y = g y)) ==> (h f x = h g x)) ==> (?! f. !x. f x = h f x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 280 Theorem LESS_EQ_REFL autoloading from theory `arithmetic` ... @@ -15130,7 +15164,7 @@ Intermediate theorems generated: 187 INSEG_WOSET = |- !l m. m inseg l /\ woset l ==> woset m -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 401 LINSEG_INSEG = |- !l a. woset l ==> (linseg l a) inseg l @@ -15177,12 +15211,12 @@ woset l /\ fl l a ==> (\(x,y). linseg l a(x,y) \/ (y = a) /\ (fl(linseg l a)x \/ (x = a))) inseg l -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 489 ORDINAL_CHAINED = |- !l m. ordinal l /\ ordinal m ==> m inseg l \/ l inseg m -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 997 FL_SUC = @@ -15198,7 +15232,7 @@ ordinal (\(x,y). l(x,y) \/ (y = (@y. ~fl l y)) /\ (fl l x \/ (x = (@y. ~fl l y)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2338 ORDINAL_UNION = |- !P. (!l. P l ==> ordinal l) ==> ordinal(Union P) @@ -15217,7 +15251,7 @@ Intermediate theorems generated: 154 WO_LEMMA = |- ?l. ordinal l /\ (!x. fl l x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 135 WO_FL_RESTRICT = @@ -15249,7 +15283,7 @@ KL_POSET_LEMMA = |- poset(\(c1,c2). C subset c1 /\ c1 subset c2 /\ chain l c2) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 386 KL = @@ -15270,7 +15304,7 @@ File mk_wellorder loaded () : void -Run time: 0.5s +Run time: 0.7s Intermediate theorems generated: 22538 #make[4]: Leaving directory '/build/hol88-2.02.19940316/Library/wellorder' @@ -15279,7 +15313,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -15410,7 +15444,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -15502,7 +15536,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -15594,12 +15628,12 @@ Run time: 0.1s Intermediate theorems generated: 6013 -===> abs_theory rebuilt on Mon Oct 25 13:41:03 -12 2021 +===> abs_theory rebuilt on Wed Sep 23 09:37:04 +14 2020 Making abs_theory.ml =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -15759,7 +15793,7 @@ File abs_theory compiled () : void -Run time: 0.0s +Run time: 0.1s make[4]: Leaving directory '/build/hol88-2.02.19940316/Library/abs_theory' make[4]: Entering directory '/build/hol88-2.02.19940316/Library/reals' @@ -15772,7 +15806,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -16015,7 +16049,7 @@ TRAT_ADD_ASSOC = |- !h i j. (h trat_add (i trat_add j)) trat_eq ((h trat_add i) trat_add j) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 297 TRAT_MUL_SYM = |- !h i. (h trat_mul i) trat_eq (i trat_mul h) @@ -16044,7 +16078,7 @@ Intermediate theorems generated: 127 TRAT_MUL_LINV = |- !h. ((trat_inv h) trat_mul h) trat_eq trat_1 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 136 Theorem ADD_INV_0_EQ autoloading from theory `arithmetic` ... @@ -16105,7 +16139,7 @@ Theorem SUB_EQ_0 autoloading from theory `arithmetic` ... SUB_EQ_0 = |- !m n. (m - n = 0) = m <= n -Run time: 0.0s +Run time: 0.1s TRAT_ARCH = |- !h. ?n d. (trat_sucint n) trat_eq (h trat_add d) Run time: 0.0s @@ -16199,7 +16233,7 @@ File hrat.ml loaded () : void -Run time: 0.2s +Run time: 0.3s Intermediate theorems generated: 11032 #\ @@ -16209,7 +16243,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -16443,7 +16477,7 @@ HRAT_GT_L1 = |- !x y. hrat_1 hrat_lt ((hrat_inv x) hrat_mul y) = x hrat_lt y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 10 HRAT_INV_MUL = @@ -16491,7 +16525,7 @@ hreal_tybij = |- (!a. hreal(cut a) = a) /\ (!r. isacut r = (cut(hreal r) = r)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 4 EQUAL_CUTS = |- !X Y. (cut X = cut Y) ==> (X = Y) @@ -16619,11 +16653,11 @@ Intermediate theorems generated: 537 HREAL_ADD_SYM = |- !X Y. X hreal_add Y = Y hreal_add X -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 124 HREAL_MUL_SYM = |- !X Y. X hreal_mul Y = Y hreal_mul X -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 124 HREAL_ADD_ASSOC = @@ -16648,7 +16682,7 @@ Intermediate theorems generated: 278 HREAL_MUL_LINV = |- !X. (hreal_inv X) hreal_mul X = hreal_1 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 485 HREAL_NOZERO = |- !X Y. ~(X hreal_add Y = X) @@ -16676,7 +16710,7 @@ Intermediate theorems generated: 837 HREAL_LT_TOTAL = |- !X Y. (X = Y) \/ X hreal_lt Y \/ Y hreal_lt X -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 492 HREAL_LT = |- !X Y. X hreal_lt Y = (?D. Y = X hreal_add D) @@ -16692,7 +16726,7 @@ |- !P. (?X. P X) /\ (?Y. !X. P X ==> X hreal_lt Y) ==> isacut(\w. ?X. P X /\ cut X w) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 349 HREAL_SUP = @@ -16709,7 +16743,7 @@ File hreal.ml loaded () : void -Run time: 0.3s +Run time: 0.5s Intermediate theorems generated: 10456 #\ @@ -16719,7 +16753,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -16994,7 +17028,7 @@ TREAL_ADD_ASSOC = |- !x y z. x treal_add (y treal_add z) = (x treal_add y) treal_add z -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 63 Theorem HREAL_MUL_ASSOC autoloading from theory `HREAL` ... @@ -17023,7 +17057,7 @@ Run time: 0.0s TREAL_MUL_LID = |- !x. (treal_1 treal_mul x) treal_eq x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 217 TREAL_ADD_LINV = |- !x. ((treal_neg x) treal_add x) treal_eq treal_0 @@ -17071,7 +17105,7 @@ |- !x y. treal_0 treal_lt x /\ treal_0 treal_lt y ==> treal_0 treal_lt (x treal_mul y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 866 treal_of_hreal = |- !x. treal_of_hreal x = x hreal_add hreal_1,hreal_1 @@ -17149,7 +17183,7 @@ TREAL_INV_WELLDEF = |- !x1 x2. x1 treal_eq x2 ==> (treal_inv x1) treal_eq (treal_inv x2) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2545 REAL_10 = |- ~(r1 = r0) @@ -17257,7 +17291,7 @@ File realax.ml loaded () : void -Run time: 0.5s +Run time: 0.6s Intermediate theorems generated: 26795 #\ @@ -17267,7 +17301,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -17519,7 +17553,7 @@ Intermediate theorems generated: 14 REAL_NEG_LMUL = |- !x y. --(x * y) = (-- x) * y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 62 REAL_NEG_RMUL = |- !x y. --(x * y) = x * (-- y) @@ -17563,7 +17597,7 @@ Intermediate theorems generated: 19 REAL_LE_TOTAL = |- !x y. x <= y \/ y <= x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 55 REAL_LET_TOTAL = |- !x y. x <= y \/ y < x @@ -17627,7 +17661,7 @@ Intermediate theorems generated: 25 REAL_NEG_GE0 = |- !x. (& 0) <= (-- x) = x <= (& 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 25 REAL_LT_NEGTOTAL = |- !x. (x = & 0) \/ (& 0) < x \/ (& 0) < (-- x) @@ -17771,7 +17805,7 @@ Intermediate theorems generated: 35 REAL_INVINV = |- !x. ~(x = & 0) ==> (inv(inv x) = x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 114 REAL_LT_IMP_NE = |- !x y. x < y ==> ~(x = y) @@ -17803,7 +17837,7 @@ Intermediate theorems generated: 29 REAL_LT_LMUL_IMP = |- !x y z. y < z /\ (& 0) < x ==> (x * y) < (x * z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 29 REAL_LINV_UNIQ = |- !x y. (x * y = & 1) ==> (x = inv y) @@ -17831,7 +17865,7 @@ Intermediate theorems generated: 17 REAL_LT_ADDR = |- !x y. x < (x + y) = (& 0) < y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 20 REAL_LT_ADDL = |- !x y. y < (x + y) = (& 0) < x @@ -17908,7 +17942,7 @@ Intermediate theorems generated: 148 REAL_INV1 = |- inv(& 1) = & 1 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 26 REAL_OVER1 = |- !x. x / (& 1) = x @@ -17920,7 +17954,7 @@ Intermediate theorems generated: 19 REAL_DIV_LZERO = |- !x. (& 0) / x = & 0 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 20 REAL_LT_NZ = |- !n. ~(& n = & 0) = (& 0) < (& n) @@ -17957,7 +17991,7 @@ Intermediate theorems generated: 268 REAL_LT_FRACTION = |- !n d. 1 num_lt n ==> ((d / (& n)) < d = (& 0) < d) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 184 Theorem NOT_SUC autoloading from theory `num` ... @@ -18002,7 +18036,7 @@ Intermediate theorems generated: 145 REAL_SUB_SUB = |- !x y. (x - y) - x = -- y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 91 REAL_LT_ADD_SUB = |- !x y z. (x + y) < z = x < (z - y) @@ -18010,7 +18044,7 @@ Intermediate theorems generated: 23 REAL_LT_SUB_RADD = |- !x y z. (x - y) < z = x < (z + y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 25 REAL_LT_SUB_LADD = |- !x y z. x < (y - z) = (x + z) < y @@ -18050,7 +18084,7 @@ Intermediate theorems generated: 58 REAL_LTE_ADD2 = |- !w x y z. w < x /\ y <= z ==> (w + y) < (x + z) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 33 REAL_LET_ADD = |- !x y. (& 0) <= x /\ (& 0) < y ==> (& 0) < (x + y) @@ -18077,7 +18111,7 @@ Intermediate theorems generated: 23 REAL_SUB_RNEG = |- !x y. x - (-- y) = x + y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 22 REAL_SUB_NEG2 = |- !x y. (-- x) - (-- y) = y - x @@ -18085,7 +18119,7 @@ Intermediate theorems generated: 40 REAL_SUB_TRIANGLE = |- !a b c. (a - b) + (b - c) = a - c -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 93 REAL_EQ_SUB_LADD = |- !x y z. (x = y - z) = (x + z = y) @@ -18128,7 +18162,7 @@ Intermediate theorems generated: 91 REAL_EQ_LMUL2 = |- !x y z. ~(x = & 0) ==> ((y = z) = (x * y = x * z)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 35 REAL_LE_MUL2 = @@ -18139,7 +18173,7 @@ Intermediate theorems generated: 345 REAL_LE_LDIV = |- !x y z. (& 0) < x /\ y <= (z * x) ==> (y / x) <= z -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 102 REAL_LE_RDIV = |- !x y z. (& 0) < x /\ (y * x) <= z ==> y <= (z / x) @@ -18165,7 +18199,7 @@ Intermediate theorems generated: 8 REAL_INV_LT1 = |- !x. (& 0) < x /\ x < (& 1) ==> (& 1) < (inv x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 290 REAL_POS_NZ = |- !x. (& 0) < x ==> ~(x = & 0) @@ -18197,11 +18231,11 @@ Intermediate theorems generated: 68 REAL_SUMSQ = |- !x y. ((x * x) + (y * y) = & 0) = (x = & 0) /\ (y = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 163 REAL_EQ_NEG = |- !x y. (-- x = -- y) = (x = y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 36 REAL_DIV_MUL2 = @@ -18226,7 +18260,7 @@ Intermediate theorems generated: 52 ABS_0 = |- abs(& 0) = & 0 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 9 ABS_1 = |- abs(& 1) = & 1 @@ -18275,7 +18309,7 @@ Intermediate theorems generated: 75 ABS_REFL = |- !x. (abs x = x) = (& 0) <= x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 156 ABS_N = |- !n. abs(& n) = & n @@ -18300,11 +18334,11 @@ Intermediate theorems generated: 29 ABS_BETWEEN1 = |- !x y z. x < z /\ (abs(y - x)) < (z - x) ==> y < z -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 102 ABS_SIGN = |- !x y. (abs(x - y)) < y ==> (& 0) < x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 22 ABS_SIGN2 = |- !x y. (abs(x - y)) < (-- y) ==> x < (& 0) @@ -18334,7 +18368,7 @@ (abs(x - x0)) < ((y0 - x0) / (& 2)) /\ (abs(y - y0)) < ((y0 - x0) / (& 2)) ==> x < y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 935 ABS_BOUNDS = |- !x k. (abs x) <= k = (-- k) <= x /\ x <= k @@ -18346,7 +18380,7 @@ Intermediate theorems generated: 175 POW_0 = |- !n. (& 0) pow (SUC n) = & 0 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 56 POW_NZ = |- !c n. ~(c = & 0) ==> ~(c pow n = & 0) @@ -18363,7 +18397,7 @@ POW_PLUS1 = |- !e. (& 0) < e ==> (!n. ((& 1) + ((& n) * e)) <= (((& 1) + e) pow n)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 298 Theorem ADD_CLAUSES autoloading from theory `arithmetic` ... @@ -18399,7 +18433,7 @@ Intermediate theorems generated: 80 POW_MUL = |- !n x y. (x * y) pow n = (x pow n) * (y pow n) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 135 REAL_LE_POW2 = |- !x. (& 0) <= (x pow 2) @@ -18436,7 +18470,7 @@ Theorem ADD1 autoloading from theory `arithmetic` ... ADD1 = |- !m. SUC m = m num_add 1 -Run time: 0.0s +Run time: 0.1s POW_2_LT = |- !n. (& n) < ((& 2) pow n) Run time: 0.0s @@ -18473,7 +18507,7 @@ |- !P. (?x. P x) /\ (?z. !x. P x ==> x < z) ==> (?s. !y. (?x. P x /\ y < x) = y < s) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 45 sup = |- !P. sup P = (@s. !y. (?x. P x /\ y < x) = y < s) @@ -18544,7 +18578,7 @@ Sum = |- (Sum(n,0)f = & 0) /\ (Sum(n,SUC m)f = (Sum(n,m)f) + (f(n num_add m))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 51 SUM_TWO = |- !f n p. (Sum(0,n)f) + (Sum(n,p)f) = Sum(0,n num_add p)f @@ -18625,7 +18659,7 @@ Intermediate theorems generated: 133 SUM_CMUL = |- !f c m n. Sum(m,n)(\n'. c * (f n')) = c * (Sum(m,n)f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 100 SUM_NEG = |- !f n d. Sum(n,d)(\n'. --(f n')) = --(Sum(n,d)f) @@ -18654,7 +18688,7 @@ |- !f g m n. (!p. m num_le p /\ p num_lt (m num_add n) ==> (f p = g p)) ==> (Sum(m,n)f = Sum(m,n)g) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 221 SUM_NSUB = @@ -18675,7 +18709,7 @@ SUM_GROUP = |- !n k f. Sum(0,n)(\m. Sum(m num_mul k,k)f) = Sum(0,n num_mul k)f -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 169 SUM_1 = |- !f n. Sum(n,1)f = f n @@ -18715,7 +18749,7 @@ Theorem LESS_ADD_SUC autoloading from theory `arithmetic` ... LESS_ADD_SUC = |- !m n. m num_lt (m num_add (SUC n)) -Run time: 0.0s +Run time: 0.1s Theorem LESS_MONO_EQ autoloading from theory `arithmetic` ... LESS_MONO_EQ = |- !m n. (SUC m) num_lt (SUC n) = m num_lt n @@ -18756,13 +18790,13 @@ Intermediate theorems generated: 206 () : void -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1 File real.ml loaded () : void -Run time: 1.7s +Run time: 2.9s Intermediate theorems generated: 23746 #\ @@ -18772,7 +18806,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -19097,7 +19131,7 @@ |- !m. open(mtop m)S = (!x. S x ==> (?e. (& 0) < e /\ (!y. (dist m(x,y)) < e ==> S y))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 38 ball = |- !m x e. B m(x,e) = (\y. (dist m(x,y)) < e) @@ -19250,13 +19284,13 @@ Intermediate theorems generated: 143 () : void -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1 File topology.ml loaded () : void -Run time: 0.2s +Run time: 0.3s Intermediate theorems generated: 4132 #\ @@ -19266,7 +19300,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -19471,7 +19505,7 @@ Run time: 0.0s DORDER_TENDSTO = |- !m x. dorder(tendsto(m,x)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 257 Definition re_subset autoloading from theory `TOPOLOGY` ... @@ -19510,7 +19544,7 @@ (x --> x0)(mtop d,g) = (!e. (& 0) < e ==> (?n. g n n /\ (!m. g m n ==> (dist d(x m,x0)) < e))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 373 Theorem METRIC_TRIANGLE autoloading from theory `TOPOLOGY` ... @@ -19640,7 +19674,7 @@ MR1_BOUNDED = |- !g f. bounded(mr1,g)f = (?k N. g N N /\ (!n. g n N ==> (abs(f n)) < k)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 331 Theorem REAL_NEG_SUB autoloading from theory `REAL` ... @@ -19738,7 +19772,7 @@ |- !g x x0. (x --> x0)(mtop mr1,g) /\ ~(x0 = & 0) ==> bounded(mr1,g)(\n. inv(x n)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 493 NET_NULL_ADD = @@ -19849,7 +19883,7 @@ dorder g ==> (!x x0. (x --> x0)(mtop mr1,g) = ((\n. --(x n)) --> (-- x0))(mtop mr1,g)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 121 NET_SUB = @@ -19981,7 +20015,7 @@ (y --> y0)(mtop mr1,g) /\ (?N. g N N /\ (!n. g n N ==> (x n) <= (y n))) ==> x0 <= y0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 400 () : void @@ -19991,7 +20025,7 @@ File nets.ml loaded () : void -Run time: 0.3s +Run time: 0.4s Intermediate theorems generated: 7389 #\ @@ -20001,7 +20035,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -20334,7 +20368,7 @@ mono f = (!m n. m num_le n ==> (f m) <= (f n)) \/ (!m n. m num_le n ==> (f m) >= (f n)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2 Theorem REAL_LE_TRANS autoloading from theory `REAL` ... @@ -20515,7 +20549,7 @@ |- !f. bounded(mr1,$num_ge)f /\ (!m n. m num_ge n ==> (f m) >= (f n)) ==> convergent f -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 910 Theorem REAL_NEGNEG autoloading from theory `REAL` ... @@ -20574,7 +20608,7 @@ Run time: 0.0s SEQ_MONOSUB = |- !s. ?f. subseq f /\ mono(\n. s(f n)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1286 SEQ_SBOUNDED = @@ -20806,7 +20840,7 @@ ((!n. (f n) <= l) /\ f --> l) /\ (!n. m <= (g n)) /\ g --> m) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2190 Theorem REAL_SUB_0 autoloading from theory `REAL` ... @@ -20820,7 +20854,7 @@ (!n. (f n) <= (g n)) /\ (\n. (f n) - (g n)) --> (& 0) ==> (?l. ((!n. (f n) <= l) /\ f --> l) /\ (!n. l <= (g n)) /\ g --> l) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 295 Theorem ADD_SYM autoloading from theory `arithmetic` ... @@ -20949,7 +20983,7 @@ Intermediate theorems generated: 2 suminf = |- !f. suminf f = (@s. f sums s) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2 SUM_SUMMABLE = |- !f l. f sums l ==> summable f @@ -20991,7 +21025,7 @@ SUM_POS_GEN = |- !f m. (!n. m num_le n ==> (& 0) <= (f n)) ==> (!n. (& 0) <= (Sum(m,n)f)) -Run time: 0.0s +Run time: 0.1s SER_POS_LE = |- !f n. @@ -21118,7 +21152,7 @@ Intermediate theorems generated: 43 SER_CDIV = |- !x x0 c. x sums x0 ==> (\n. (x n) / c) sums (x0 / c) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 35 Theorem SUM_DIFF autoloading from theory `REAL` ... @@ -21129,7 +21163,7 @@ |- !f. summable f = (!e. (& 0) < e ==> (?N. !m n. m num_ge N ==> (abs(Sum(m,n)f)) < e)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 412 SER_ZERO = |- !f. summable f ==> f --> (& 0) @@ -21238,7 +21272,7 @@ Run time: 0.0s GP = |- !x. (abs x) < (& 1) ==> (\n. x pow n) sums (inv((& 1) - x)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 343 Theorem REAL_NEG_LMUL autoloading from theory `REAL` ... @@ -21279,13 +21313,13 @@ Intermediate theorems generated: 683 () : void -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1 File seq.ml loaded () : void -Run time: 0.6s +Run time: 0.7s Intermediate theorems generated: 18704 #\ @@ -21295,7 +21329,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -21519,7 +21553,7 @@ (!x y x0 y0. (x tends x0)(mtop mr1,g) /\ (y tends y0)(mtop mr1,g) ==> ((\n. (x n) * (y n)) tends (x0 * y0))(mtop mr1,g)) -Run time: 0.1s +Run time: 0.0s LIM_MUL = |- !f g l m. @@ -21547,7 +21581,7 @@ (!x x0. (x tends x0)(mtop mr1,g) /\ ~(x0 = & 0) ==> ((\n. inv(x n)) tends (inv x0))(mtop mr1,g)) -Run time: 0.0s +Run time: 0.1s LIM_INV = |- !f l. (f --> l)x /\ ~(l = & 0) ==> ((\x. inv(f x)) --> (inv l))x @@ -21717,7 +21751,7 @@ Intermediate theorems generated: 29 CONT_MUL = |- !x. f contl x /\ g contl x ==> (\x. (f x) * (g x)) contl x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 29 CONT_NEG = |- !x. f contl x ==> (\x. --(f x)) contl x @@ -21825,7 +21859,7 @@ ((f a) <= y /\ y <= (f b)) /\ (!x. a <= x /\ x <= b ==> f contl x) ==> (?x. a <= x /\ x <= b /\ (f x = y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2647 Theorem REAL_NEGNEG autoloading from theory `REAL` ... @@ -22046,7 +22080,7 @@ Theorem num_CASES autoloading from theory `arithmetic` ... num_CASES = |- !m. (m = 0) \/ (?n. m = SUC n) -Run time: 0.0s +Run time: 0.1s Theorem ADD_SUB autoloading from theory `arithmetic` ... ADD_SUB = |- !a c. (a num_add c) num_sub c = a @@ -22239,7 +22273,7 @@ (?M. (!x. a <= x /\ x <= b ==> (f x) <= M) /\ (?x. a <= x /\ x <= b /\ (f x = M))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1646 CONT_ATTAINS2 = @@ -22248,7 +22282,7 @@ (?M. (!x. a <= x /\ x <= b ==> M <= (f x)) /\ (?x. a <= x /\ x <= b /\ (f x = M))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 177 Theorem ABS_SIGN autoloading from theory `REAL` ... @@ -22347,7 +22381,7 @@ (!x. a <= x /\ x <= b ==> f contl x) /\ (!x. a < x /\ x < b ==> f differentiable x) ==> (?z. a < z /\ z < b /\ (f diffl (& 0))z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 3178 gfn = "\x. (f x) - ((((f b) - (f a)) / (b - a)) * x)" : term @@ -22379,7 +22413,7 @@ (!x. a < x /\ x < b ==> f differentiable x) ==> (?l z. a < z /\ z < b /\ (f diffl l)z /\ ((f b) - (f a) = (b - a) * l)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 612 DIFF_ISCONST_END = @@ -22411,7 +22445,7 @@ File lim.ml loaded () : void -Run time: 0.6s +Run time: 0.8s Intermediate theorems generated: 21608 #\ @@ -22421,7 +22455,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -22530,7 +22564,7 @@ Intermediate theorems generated: 47 () : void -Run time: 0.0s +Run time: 0.1s Definition pow autoloading from theory `REAL` ... pow = |- (!x. x pow 0 = & 1) /\ (!x n. x pow (SUC n) = x * (x pow n)) @@ -22554,7 +22588,7 @@ Theorem LESS_THM autoloading from theory `prim_rec` ... LESS_THM = |- !m n. m num_lt (SUC n) = (m = n) \/ m num_lt n -Run time: 0.1s +Run time: 0.0s Theorem NOT_LESS autoloading from theory `arithmetic` ... NOT_LESS = |- !m n. ~m num_lt n = n num_le m @@ -22867,7 +22901,7 @@ Sum(0,n)(\n. (& n) * ((c n) * (x pow (n num_sub 1)))) = (Sum(0,n)(\n. (diffs c n) * (x pow n))) - ((& n) * ((c n) * (x pow (n num_sub 1)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 34 Theorem REAL_SUB_RZERO autoloading from theory `REAL` ... @@ -22992,7 +23026,7 @@ (\q. ((z + h) pow q) * (z pow (((n num_sub 2) num_sub p) num_sub q))))))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 866 Theorem INV_SUC_EQ autoloading from theory `prim_rec` ... @@ -23261,7 +23295,7 @@ |- !f l x. (f diffl l)x = ((\h. ((f(x + h)) - (f x)) / h) tends_real_real l)(& 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1 TERMDIFF = @@ -23273,7 +23307,7 @@ ((\x. suminf(\n. (c n) * (x pow n))) diffl (suminf(\n. (diffs c n) * (x pow n)))) x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2494 () : void @@ -23283,7 +23317,7 @@ File powser.ml loaded () : void -Run time: 0.3s +Run time: 0.4s Intermediate theorems generated: 8507 #\ @@ -23293,7 +23327,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -23379,7 +23413,7 @@ Theory POWSER loaded () : void -Run time: 0.0s +Run time: 0.1s Theorem ADD_CLAUSES autoloading from theory `arithmetic` ... ADD_CLAUSES = @@ -23461,7 +23495,7 @@ Intermediate theorems generated: 48 () : void -Run time: 0.1s +Run time: 0.0s basic_diffs = [] : thm list Run time: 0.0s @@ -23806,7 +23840,7 @@ Theorem REAL_MUL_RZERO autoloading from theory `REAL` ... REAL_MUL_RZERO = |- !x. x * (& 0) = & 0 -Run time: 0.0s +Run time: 0.1s Definition EVEN autoloading from theory `arithmetic` ... EVEN = |- (EVEN 0 = T) /\ (!n. EVEN(SUC n) = ~EVEN n) @@ -23993,7 +24027,7 @@ Run time: 0.0s EXP_LE_X = |- !x. (& 0) <= x ==> ((& 1) + x) <= (exp x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 420 EXP_LT_1 = |- !x. (& 0) < x ==> (& 1) < (exp x) @@ -24313,7 +24347,7 @@ Run time: 0.0s COS_0 = |- cos(& 0) = & 1 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 454 SIN_CIRCLE = |- !x. ((sin x) pow 2) + ((cos x) pow 2) = & 1 @@ -24369,7 +24403,7 @@ Run time: 0.0s COS_BOUND = |- !x. (abs(cos x)) <= (& 1) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 160 COS_BOUNDS = |- !x. (--(& 1)) <= (cos x) /\ (cos x) <= (& 1) @@ -24412,7 +24446,7 @@ |- !x. (((sin(-- x)) + (sin x)) pow 2) + (((cos(-- x)) - (cos x)) pow 2) = & 0 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1099 Theorem REAL_SUMSQ autoloading from theory `REAL` ... @@ -24522,7 +24556,7 @@ Run time: 0.0s SIN_POS = |- !x. (& 0) < x /\ x < (& 2) ==> (& 0) < (sin x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2052 COS_PAIRED = @@ -24531,7 +24565,7 @@ (((--(& 1)) pow n) / (&(FACT(2 num_mul n)))) * (x pow (2 num_mul n))) sums (cos x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 163 Theorem LESS_MONO_EQ autoloading from theory `arithmetic` ... @@ -24618,7 +24652,7 @@ Intermediate theorems generated: 2 PI2 = |- pi / (& 2) = (@x. (& 0) <= x /\ x <= (& 2) /\ (cos x = & 0)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 117 COS_PI2 = |- cos(pi / (& 2)) = & 0 @@ -24678,7 +24712,7 @@ Intermediate theorems generated: 59 SIN_PERIODIC = |- !x. sin(x + ((& 2) * pi)) = sin x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 47 COS_PERIODIC = |- !x. cos(x + ((& 2) * pi)) = cos x @@ -24761,7 +24795,7 @@ |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (?! x. (--(pi / (& 2))) <= x /\ x <= (pi / (& 2)) /\ (sin x = y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 431 Theorem REAL_DIV_RMUL autoloading from theory `REAL` ... @@ -24838,7 +24872,7 @@ (sin x = & 0) = (?n. EVEN n /\ (x = (& n) * (pi / (& 2)))) \/ (?n. EVEN n /\ (x = --((& n) * (pi / (& 2))))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 319 tan = |- !x. tan x = (sin x) / (cos x) @@ -24858,7 +24892,7 @@ Intermediate theorems generated: 24 TAN_NEG = |- !x. tan(-- x) = --(tan x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 46 TAN_PERIODIC = |- !x. tan(x + ((& 2) * pi)) = tan x @@ -24947,13 +24981,13 @@ TAN_TOTAL_LEMMA = |- !y. (& 0) < y ==> (?x. (& 0) < x /\ x < (pi / (& 2)) /\ y < (tan x)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1046 TAN_TOTAL_POS = |- !y. (& 0) <= y ==> (?x. (& 0) <= x /\ x < (pi / (& 2)) /\ (tan x = y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 372 Theorem POW_NZ autoloading from theory `REAL` ... @@ -25028,7 +25062,7 @@ Intermediate theorems generated: 79 ACS_COS = |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (cos(acs y) = y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 18 ACS_BOUNDS = @@ -25054,7 +25088,7 @@ Intermediate theorems generated: 28 ATN_BOUNDS = |- !y. (--(pi / (& 2))) < (atn y) /\ (atn y) < (pi / (& 2)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 28 TAN_ATN = @@ -25069,7 +25103,7 @@ File transc.ml loaded () : void -Run time: 1.0s +Run time: 1.3s Intermediate theorems generated: 30503 #make[5]: Leaving directory '/build/hol88-2.02.19940316/Library/reals/theories' @@ -25082,7 +25116,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -25104,7 +25138,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -25170,7 +25204,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -25202,7 +25236,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -25311,7 +25345,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -25464,7 +25498,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -25537,7 +25571,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -25617,7 +25651,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -25774,7 +25808,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -25929,7 +25963,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -26146,7 +26180,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -26168,7 +26202,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -26187,7 +26221,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -26232,7 +26266,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -26297,7 +26331,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -26347,7 +26381,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -26417,7 +26451,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -26487,7 +26521,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -26523,7 +26557,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -26576,7 +26610,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -26648,7 +26682,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -26727,7 +26761,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -26922,7 +26956,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -26959,7 +26993,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -27645,7 +27679,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -28117,7 +28151,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -28381,7 +28415,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -28626,7 +28660,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -29090,7 +29124,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -29558,7 +29592,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -29614,7 +29648,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -29704,7 +29738,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -29903,7 +29937,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -29935,7 +29969,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -30069,7 +30103,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -30372,7 +30406,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -30404,7 +30438,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -30443,7 +30477,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -30475,7 +30509,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -30636,7 +30670,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -30769,7 +30803,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -30958,7 +30992,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -31018,7 +31052,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -31143,7 +31177,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -31254,7 +31288,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -31279,7 +31313,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -31307,7 +31341,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -31420,7 +31454,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -31923,7 +31957,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -32171,7 +32205,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -32397,7 +32431,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -32439,7 +32473,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -32471,7 +32505,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -32694,7 +32728,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -33087,7 +33121,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -33200,7 +33234,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -33703,7 +33737,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -33951,7 +33985,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -34177,7 +34211,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -34212,7 +34246,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -34251,7 +34285,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -34288,7 +34322,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -34309,7 +34343,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -34406,7 +34440,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -34428,7 +34462,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -34924,7 +34958,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -34947,7 +34981,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -35025,7 +35059,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -35084,7 +35118,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -35128,7 +35162,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -35146,7 +35180,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -35173,7 +35207,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -35217,7 +35251,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -35330,7 +35364,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -35377,7 +35411,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -35416,7 +35450,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -35490,7 +35524,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -35579,7 +35613,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -35650,7 +35684,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -35720,7 +35754,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -35769,7 +35803,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -35810,7 +35844,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -35851,7 +35885,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -35875,7 +35909,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -35976,7 +36010,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -35997,7 +36031,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -36022,7 +36056,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -36648,7 +36682,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -36725,7 +36759,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -36752,7 +36786,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -36869,7 +36903,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -36964,7 +36998,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -37050,7 +37084,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -37165,7 +37199,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -37258,7 +37292,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -37434,7 +37468,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -37538,7 +37572,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -37833,7 +37867,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -37936,7 +37970,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -38004,7 +38038,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -38066,7 +38100,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -38246,7 +38280,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -38287,7 +38321,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -38317,7 +38351,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -38343,7 +38377,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -38861,7 +38895,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -39398,7 +39432,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -39586,7 +39620,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 + HOL88 Version 2.02 (GCL), built on 23/9/20 =============================================================================== #false : bool @@ -39604,10 +39638,10 @@ =======> library rebuilt make[3]: Leaving directory '/build/hol88-2.02.19940316/Library' date -Mon Oct 25 13:44:14 -12 2021 +Wed Sep 23 09:41:04 +14 2020 make[2]: Leaving directory '/build/hol88-2.02.19940316' date -Mon Oct 25 13:44:14 -12 2021 +Wed Sep 23 09:41:04 +14 2020 make permissions make[2]: Entering directory '/build/hol88-2.02.19940316' find $(ls -1 | grep -v debian) \ @@ -39625,22 +39659,22 @@ printf 'install `'/usr/share/hol88-2.02.19940316'`;;\nlisp `(ml-save "foo")`;;\n' | ./$i &&\ mv foo $i; done - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 25/10/21 -=============================================================================== +HOL-LCF version 2.02 (GCL) created 23/9/20 #HOL installed (`/usr/share/hol88-2.02.19940316`) () : void # -HOL-LCF version 2.02 (GCL) created 25/10/21 + +=============================================================================== + HOL88 Version 2.02 (GCL), built on 23/9/20 +=============================================================================== #HOL installed (`/usr/share/hol88-2.02.19940316`) () : void # -BASIC-HOL version 2.02 (GCL) created 25/10/21 +BASIC-HOL version 2.02 (GCL) created 23/9/20 #HOL installed (`/usr/share/hol88-2.02.19940316`) () : void @@ -39987,7 +40021,7 @@ ### simple group (level 1) entered at line 168 ({) ### bottom level (see the transcript file for additional information) -Output written on tutorial.dvi (112 pages, 310276 bytes). +Output written on tutorial.dvi (112 pages, 310280 bytes). Transcript written on tutorial.log. make[4]: Leaving directory '/build/hol88-2.02.19940316/Manual/Tutorial' make[4]: Entering directory '/build/hol88-2.02.19940316/Manual/Tutorial' @@ -40096,7 +40130,7 @@ ### simple group (level 1) entered at line 168 ({) ### bottom level (see the transcript file for additional information) -Output written on tutorial.dvi (114 pages, 332084 bytes). +Output written on tutorial.dvi (114 pages, 332088 bytes). Transcript written on tutorial.log. make[4]: Leaving directory '/build/hol88-2.02.19940316/Manual/Tutorial' make[3]: Leaving directory '/build/hol88-2.02.19940316/Manual/Tutorial' @@ -41369,12 +41403,12 @@ ) (see the transcript file for additional information) -Output written on description.dvi (346 pages, 995624 bytes). +Output written on description.dvi (346 pages, 995628 bytes). Transcript written on description.log. make[4]: Leaving directory '/build/hol88-2.02.19940316/Manual/Description' make[4]: Entering directory '/build/hol88-2.02.19940316/Manual/Description' ../LaTeX/makeindex ../../ description.idx index.tex -../LaTeX/makeindex: 1: ../LaTeX/makeindex: /bin/arch: not found +../LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -41579,7 +41613,7 @@ (./drules.aux) (./conv.aux) (./tactics.aux) (./see.aux) (./references.aux) (./version2.aux) (./index.aux)) ) (see the transcript file for additional information) -Output written on description.dvi (353 pages, 1078852 bytes). +Output written on description.dvi (353 pages, 1078856 bytes). Transcript written on description.log. make[4]: Leaving directory '/build/hol88-2.02.19940316/Manual/Description' make[3]: Leaving directory '/build/hol88-2.02.19940316/Manual/Description' @@ -43131,12 +43165,12 @@ (./reference.aux (./title.aux) (./preface.aux) (./ack.aux) (./contents.aux) (./entries.aux) (./theorems.aux) (./index.aux)) ) (see the transcript file for additional information) -Output written on reference.dvi (669 pages, 1132376 bytes). +Output written on reference.dvi (669 pages, 1132384 bytes). Transcript written on reference.log. make[4]: Leaving directory '/build/hol88-2.02.19940316/Manual/Reference' make[4]: Entering directory '/build/hol88-2.02.19940316/Manual/Reference' ../LaTeX/makeindex ../../ reference.idx index.tex -../LaTeX/makeindex: 1: ../LaTeX/makeindex: /bin/arch: not found +../LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -44662,7 +44696,7 @@ (./reference.aux (./title.aux) (./preface.aux) (./ack.aux) (./contents.aux) (./entries.aux) (./theorems.aux) (./index.aux)) ) (see the transcript file for additional information) -Output written on reference.dvi (669 pages, 1136848 bytes). +Output written on reference.dvi (669 pages, 1136852 bytes). Transcript written on reference.log. make[4]: Leaving directory '/build/hol88-2.02.19940316/Manual/Reference' make[3]: Leaving directory '/build/hol88-2.02.19940316/Manual/Reference' @@ -44877,7 +44911,7 @@ make[6]: Entering directory '/build/hol88-2.02.19940316/Library/abs_theory/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ abs_theory.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45130,7 +45164,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/arith/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/arith/Manual' ../../../Manual/LaTeX/makeindex ../../../ arith.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45365,7 +45399,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/finite_sets/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/finite_sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ finite_sets.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45540,7 +45574,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/more_arithmetic/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/more_arithmetic/Manual' ../../../Manual/LaTeX/makeindex ../../../ more_arithmetic.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45726,7 +45760,7 @@ make[6]: Entering directory '/build/hol88-2.02.19940316/Library/numeral/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ numeral.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45844,7 +45878,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/pair/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/pair/Manual' ../../../Manual/LaTeX/makeindex ../../../ index.tex pair -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45959,7 +45993,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/parser/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/parser/Manual' ../../../Manual/LaTeX/makeindex ../../../ parser.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46197,7 +46231,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/pred_sets/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/pred_sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ pred_sets.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46536,7 +46570,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/prettyp/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/prettyp/Manual' ../../../Manual/LaTeX/makeindex ../../../ prettyp.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46741,7 +46775,7 @@ make[6]: Entering directory '/build/hol88-2.02.19940316/Library/reals/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ reals.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47079,7 +47113,7 @@ make[6]: Entering directory '/build/hol88-2.02.19940316/Library/reduce/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ reduce.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47268,7 +47302,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/res_quan/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/res_quan/Manual' ../../../Manual/LaTeX/makeindex ../../../ res_quan.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47534,7 +47568,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/sets/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ sets.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47693,7 +47727,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/string/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/string/Manual' ../../../Manual/LaTeX/makeindex ../../../ string.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47836,7 +47870,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/taut/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/taut/Manual' ../../../Manual/LaTeX/makeindex ../../../ taut.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47986,7 +48020,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/trs/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/trs/Manual' ../../../Manual/LaTeX/makeindex ../../../ trs.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48140,7 +48174,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/unwind/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/unwind/Manual' ../../../Manual/LaTeX/makeindex ../../../ unwind.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48316,7 +48350,7 @@ make[6]: Entering directory '/build/hol88-2.02.19940316/Library/wellorder/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ wellorder.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48509,7 +48543,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/window/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/window/Manual' ../../../Manual/LaTeX/makeindex ../../../ window.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48731,7 +48765,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/word/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/word/Manual' ../../../Manual/LaTeX/makeindex ../../../ word.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48922,7 +48956,7 @@ ) (/usr/share/texlive/texmf-dist/tex/latex/base/ulasy.fd) [1] [2]) (./preface.tex) [3] (./libraries.aux (./title.aux) (./preface.aux)) ) -Output written on libraries.dvi (3 pages, 2236 bytes). +Output written on libraries.dvi (3 pages, 2244 bytes). Transcript written on libraries.log. make[4]: Leaving directory '/build/hol88-2.02.19940316/Manual/Libraries' make[3]: Leaving directory '/build/hol88-2.02.19940316/Manual/Libraries' @@ -48988,7 +49022,7 @@ ===> endpages.dvi created dvips endpages > endpages.ps This is dvips(k) 5.998 Copyright 2018 Radical Eye Software (www.radicaleye.com) -' TeX output 2021.10.25:1347' -> endpages.ps +' TeX output 2020.09.23:0942' -> endpages.ps . @@ -49049,7 +49083,7 @@ ===> titlepages.dvi created dvips titlepages > titlepages.ps This is dvips(k) 5.998 Copyright 2018 Radical Eye Software (www.radicaleye.com) -' TeX output 2021.10.25:1347' -> titlepages.ps +' TeX output 2020.09.23:0942' -> titlepages.ps . @@ -49152,13 +49186,13 @@ dh_gencontrol dh_md5sums dh_builddeb +dpkg-deb: building package 'hol88-library-source' in '../hol88-library-source_2.02.19940316-35_all.deb'. dpkg-deb: building package 'hol88-source' in '../hol88-source_2.02.19940316-35_all.deb'. +dpkg-deb: building package 'hol88-doc' in '../hol88-doc_2.02.19940316-35_all.deb'. dpkg-deb: building package 'hol88-contrib-source' in '../hol88-contrib-source_2.02.19940316-35_all.deb'. -dpkg-deb: building package 'hol88-help' in '../hol88-help_2.02.19940316-35_all.deb'. -dpkg-deb: building package 'hol88-library-help' in '../hol88-library-help_2.02.19940316-35_all.deb'. dpkg-deb: building package 'hol88-contrib-help' in '../hol88-contrib-help_2.02.19940316-35_all.deb'. -dpkg-deb: building package 'hol88-doc' in '../hol88-doc_2.02.19940316-35_all.deb'. -dpkg-deb: building package 'hol88-library-source' in '../hol88-library-source_2.02.19940316-35_all.deb'. +dpkg-deb: building package 'hol88-library-help' in '../hol88-library-help_2.02.19940316-35_all.deb'. +dpkg-deb: building package 'hol88-help' in '../hol88-help_2.02.19940316-35_all.deb'. make[1]: Leaving directory '/build/hol88-2.02.19940316' dpkg-genbuildinfo --build=binary dpkg-genchanges --build=binary >../hol88_2.02.19940316-35_i386.changes @@ -49166,12 +49200,14 @@ dpkg-source --after-build . dpkg-buildpackage: info: binary-only upload (no source included) I: copying local configuration +I: user script /srv/workspace/pbuilder/22984/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/22984/tmp/hooks/B01_cleanup finished I: unmounting dev/ptmx filesystem I: unmounting dev/pts filesystem I: unmounting dev/shm filesystem I: unmounting proc filesystem I: unmounting sys filesystem I: cleaning the build env -I: removing directory /srv/workspace/pbuilder/5314 and its subdirectories -I: Current time: Mon Oct 25 13:49:36 -12 2021 -I: pbuilder-time-stamp: 1635212976 +I: removing directory /srv/workspace/pbuilder/22984 and its subdirectories +I: Current time: Wed Sep 23 09:43:43 +14 2020 +I: pbuilder-time-stamp: 1600803823