diff options
| author | Edwin Groothuis <edwin@FreeBSD.org> | 2008-08-15 04:33:04 +0000 |
|---|---|---|
| committer | Edwin Groothuis <edwin@FreeBSD.org> | 2008-08-15 04:33:04 +0000 |
| commit | 0002baf18813f5041ee75b5ec58dbe402be8aadc (patch) | |
| tree | 8ef73fea6ccf16a0585301ef5f8f299d4b08b1cc /math | |
| parent | 3baea6f442c7e9e4fef51751b4abb2eddee111a9 (diff) | |
| download | ports-0002baf18813f5041ee75b5ec58dbe402be8aadc.tar.gz ports-0002baf18813f5041ee75b5ec58dbe402be8aadc.zip | |
Notes
Diffstat (limited to 'math')
52 files changed, 320 insertions, 1653 deletions
diff --git a/math/isabelle/Makefile b/math/isabelle/Makefile index 06ec0678ce8d..44e5e2900602 100644 --- a/math/isabelle/Makefile +++ b/math/isabelle/Makefile @@ -6,50 +6,122 @@ # PORTNAME= isabelle -PORTVERSION= 2007 -PORTREVISION= 1 +PORTVERSION= 2008 CATEGORIES= math MASTER_SITES= http://isabelle.in.tum.de/dist/ \ http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/ \ http://mirror.cse.unsw.edu.au/pub/isabelle/dist/ -DISTNAME= Isabelle2007 +DISTNAME= Isabelle2008 .if !defined(NOPORTDOCS) -DISTFILES= Isabelle2007.tar.gz \ - Isabelle2007_library.tar.gz \ - Isabelle2007_pdf.tar.gz +DISTFILES= Isabelle2008.tar.gz \ + Isabelle2008_library.tar.gz \ + Isabelle2008_pdf.tar.gz .endif MAINTAINER= timbob@bigpond.com COMMENT= A generic proof assistant -OPTIONS= SMLNJ "Use SML/NJ (devel) instead of the faster Poly/ML" off +OPTIONS= SMLNJ "Use SML/NJ (devel) instead of faster Poly/ML" off +OPTIONS+= RLWRAP "Use rlwrap as line editor" on +OPTIONS+= LEDIT "Use ledit as line editor" off +OPTIONS+= HOL_ALGEBRA "Build optional heap: HOL-Algebra" off +OPTIONS+= HOL_COMPLEX "Build optional heap: HOL-Complex" off +OPTIONS+= HOL_MATRIX "Build optional heap: HOL-Complex-Matrix" off +OPTIONS+= HOL_NOMINAL "Build optional heap: HOL-Nominal" off +OPTIONS+= HOL_WORD "Build optional heap: HOL-Word" off +OPTIONS+= HOL_TLA "Build optional heap: TLA" off +OPTIONS+= HOL_HOL4 "Build optional heap: HOL4" off +OPTIONS+= HOLCF_IOA "Build optional heap: IOA" off USE_PERL5= yes +BUILD_DEPENDS+= bash:${PORTSDIR}/shells/bash RUN_DEPENDS+= proofgeneral:${PORTSDIR}/math/proofgeneral +RUN_DEPENDS+= bash:${PORTSDIR}/shells/bash DOCFILES= Contents *.pdf *.eps *.ps *.dvi .include <bsd.port.pre.mk> +.if defined(WITH_RLWRAP) +RUN_DEPENDS+= rlwrap:${PORTSDIR}/devel/rlwrap +LINE_EDIT= "${PREFIX}/bin/rlwrap" +.else +.if defined(WITH_LEDIT) +RUN_DEPENDS+= ledit:${PORTSDIR}/sysutils/ledit +LINE_EDIT= "${PREFIX}/bin/ledit" +.else +LINE_EDIT= "" +.endif +.endif + +.if defined(WITH_HOL_ALGEBRA) +HEAP_HOL_ALGEBRA="" +.else +HEAP_HOL_ALGEBRA="@comment " +.endif +.if defined(WITH_HOL_COMPLEX) +HEAP_HOL_COMPLEX="" +.else +HEAP_HOL_COMPLEX="@comment " +.endif +.if defined(WITH_HOL_MATRIX) +HEAP_HOL_COMPLEX_MATRIX="" +.else +HEAP_HOL_COMPLEX_MATRIX="@comment " +.endif +.if defined(WITH_HOL_NOMINAL) +HEAP_HOL_NOMINAL="" +.else +HEAP_HOL_NOMINAL="@comment " +.endif +.if defined(WITH_HOL_WORD) +HEAP_HOL_WORD="" +.else +HEAP_HOL_WORD="@comment " +.endif +.if defined(WITH_HOL_TLA) +HEAP_HOL_TLA="" +.else +HEAP_HOL_TLA="@comment " +.endif +.if defined(WITH_HOL_HOL4) +HEAP_HOL_HOL4="" +.else +HEAP_HOL_HOL4="@comment " +.endif +.if defined(WITH_HOLCF_IOA) +HEAP_HOLCF_IOA="" +.else +HEAP_HOLCF_IOA="@comment " +.endif + .if defined(WITH_SMLNJ) ML_SYSTEM= smlnj-110 ML_HOME= ${LOCALBASE}/bin ML_OPTIONS= @SMLdebug=/dev/null .else -ML_SYSTEM= polyml-5.1 +ML_SYSTEM= polyml-5.2 ML_HOME= ${LOCALBASE}/bin ML_OPTIONS= -H 500 ML_DBASE= "" .endif ML_PLATFORM= x86-bsd -PLIST_SUB= HEAPSUBDIR=${ML_SYSTEM}_${ML_PLATFORM} +PLIST_SUB= HEAPSUBDIR=${ML_SYSTEM}_${ML_PLATFORM} \ + HEAP_HOL_ALGEBRA=${HEAP_HOL_ALGEBRA} \ + HEAP_HOL_COMPLEX=${HEAP_HOL_COMPLEX} \ + HEAP_HOL_COMPLEX_MATRIX=${HEAP_HOL_COMPLEX_MATRIX} \ + HEAP_HOL_NOMINAL=${HEAP_HOL_NOMINAL} \ + HEAP_HOL_WORD=${HEAP_HOL_WORD} \ + HEAP_HOL_TLA=${HEAP_HOL_TLA} \ + HEAP_HOL_HOL4=${HEAP_HOL_HOL4} \ + HEAP_HOLCF_IOA=${HEAP_HOLCF_IOA} .if defined(WITH_SMLNJ) BUILD_DEPENDS+= smlnj-devel>=110.65:${PORTSDIR}/lang/sml-nj-devel MAKE_ENV+= SMLNJ_DEVEL=yes .else -BUILD_DEPENDS+= poly:${PORTSDIR}/lang/polyml -RUN_DEPENDS+= poly:${PORTSDIR}/lang/polyml +BUILD_DEPENDS+= polyml>=5.2:${PORTSDIR}/lang/polyml +RUN_DEPENDS+= polyml>=5.2:${PORTSDIR}/lang/polyml .endif NO_INSTALL_MANPAGES=yes @@ -64,13 +136,40 @@ post-patch: s|%%ML_OPTIONS%%|\"${ML_OPTIONS}\"|; \ s|%%ML_DBASE%%|${ML_DBASE}|; \ s|%%ML_PLATFORM%%|${ML_PLATFORM}|; \ - s|%%PREFIX%%|${PREFIX}|" \ + s|%%PREFIX%%|${PREFIX}|; \ + s|%%LINE_EDIT%%|${LINE_EDIT}|" \ ${WRKSRC}/etc/settings.presed > ${WRKSRC}/etc/settings @${RM} ${WRKSRC}/etc/settings.presed @${TOUCH} ${WRKSRC}/contrib/.keep @${REINPLACE_CMD} -e 's|%%SMLNJ_VERSION%%|SMLNJ_DEVEL=yes|' \ ${WRKSRC}/lib/scripts/run-smlnj +post-build: +.if defined(WITH_HOL_ALGEBRA) + ${WRKSRC}/build -b -m HOL-Algebra HOL +.endif +.if defined(WITH_HOL_COMPLEX) + ${WRKSRC}/build -b -m HOL-Complex HOL +.endif +.if defined(WITH_HOL_MATRIX) + ${WRKSRC}/build -b -m HOL-Complex-Matrix HOL +.endif +.if defined(WITH_HOL_NOMINAL) + ${WRKSRC}/build -b -m HOL-Nominal HOL +.endif +.if defined(WITH_HOL_WORD) + ${WRKSRC}/build -b -m HOL-Word HOL +.endif +.if defined(WITH_HOL_TLA) + ${WRKSRC}/build -b -m TLA HOL +.endif +.if defined(WITH_HOL_HOL4) + ${WRKSRC}/build -b -m HOL4 HOL +.endif +.if defined(WITH_HOLCF_IOA) + ${WRKSRC}/build -b -m IOA HOLCF +.endif + post-install: ${WRKSRC}/bin/isatool ${INSTALL} -d ${PREFIX}/share/isabelle -p ${PREFIX}/bin .if !defined(NOPORTDOCS) diff --git a/math/isabelle/distinfo b/math/isabelle/distinfo index 9eb6d3784b3d..2c65b9b111e4 100644 --- a/math/isabelle/distinfo +++ b/math/isabelle/distinfo @@ -1,9 +1,9 @@ -MD5 (Isabelle2007.tar.gz) = 088e56b79a4c8cd3e4de7dad62a35827 -SHA256 (Isabelle2007.tar.gz) = eb270bc44ddb8195c6b80eb80894555671119d12b7aa8d2aa31d1b2149604f26 -SIZE (Isabelle2007.tar.gz) = 7577495 -MD5 (Isabelle2007_library.tar.gz) = a257ee276275619832748c07cf0257b5 -SHA256 (Isabelle2007_library.tar.gz) = b0f407e69d6406d0313c5d0c3a030267908e43b134532eb836fc6236ed440647 -SIZE (Isabelle2007_library.tar.gz) = 37173555 -MD5 (Isabelle2007_pdf.tar.gz) = b7b0f6965dc3e9f2a88c35d2f3c0cad7 -SHA256 (Isabelle2007_pdf.tar.gz) = a9d34030f17d28420bdddecd661e2664c7db1171f278fdbf0f10c7daf3fded32 -SIZE (Isabelle2007_pdf.tar.gz) = 6024675 +MD5 (Isabelle2008.tar.gz) = 4ebd3288458b6a87979b211bf8fe3e15 +SHA256 (Isabelle2008.tar.gz) = 27c963524992d88af57184a19ede96325bd8c117bd29d86664d25183dfffc140 +SIZE (Isabelle2008.tar.gz) = 7932744 +MD5 (Isabelle2008_library.tar.gz) = feff661e1b5e7279f3dedb9924e03973 +SHA256 (Isabelle2008_library.tar.gz) = a5b6d8d22b004b14e94ef8fa16de272b669888a4847f512dbb7874b531612aba +SIZE (Isabelle2008_library.tar.gz) = 37598185 +MD5 (Isabelle2008_pdf.tar.gz) = e52b6f445b06a4a0b7c90d703196c37d +SHA256 (Isabelle2008_pdf.tar.gz) = 71b98cb7ae0e5a2d9645e16d2f1f274cc5626ffade96d248ac48529329c79bf7 +SIZE (Isabelle2008_pdf.tar.gz) = 5214045 diff --git a/math/isabelle/files/patch-bin-Isabelle b/math/isabelle/files/patch-bin-Isabelle deleted file mode 100644 index 86b306d14cee..000000000000 --- a/math/isabelle/files/patch-bin-Isabelle +++ /dev/null @@ -1,8 +0,0 @@ ---- ./bin/Isabelle.orig Sun Sep 2 15:23:58 2007 -+++ ./bin/Isabelle Sun Sep 2 16:05:40 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: Isabelle,v 1.30 2005/05/17 07:58:47 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen diff --git a/math/isabelle/files/patch-bin-isabelle b/math/isabelle/files/patch-bin-isabelle deleted file mode 100644 index 62b441a378bb..000000000000 --- a/math/isabelle/files/patch-bin-isabelle +++ /dev/null @@ -1,8 +0,0 @@ ---- ./bin/isabelle.orig Sun Sep 2 15:23:58 2007 -+++ ./bin/isabelle Sun Sep 2 16:05:44 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: isabelle,v 1.46 2005/05/17 07:58:47 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen diff --git a/math/isabelle/files/patch-bin-isabelle_interface b/math/isabelle/files/patch-bin-isabelle_interface deleted file mode 100644 index a8ec33a1f2a3..000000000000 --- a/math/isabelle/files/patch-bin-isabelle_interface +++ /dev/null @@ -1,23 +0,0 @@ ---- ./bin/isabelle-interface.orig Sun Sep 2 15:23:58 2007 -+++ ./bin/isabelle-interface Sun Sep 2 16:05:48 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: isabelle-interface,v 1.8 2005/05/17 16:10:33 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -16,12 +16,12 @@ - PRG="$(basename "$0")" - - ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)" --source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 -+. "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 - - - ## diagnostics - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 diff --git a/math/isabelle/files/patch-bin-isabelle_process b/math/isabelle/files/patch-bin-isabelle_process deleted file mode 100644 index 92c308f02e7e..000000000000 --- a/math/isabelle/files/patch-bin-isabelle_process +++ /dev/null @@ -1,32 +0,0 @@ ---- bin/isabelle-process.orig Sat Jan 12 16:42:22 2008 -+++ bin/isabelle-process Sat Jan 12 16:42:58 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: isabelle-process,v 1.17 2006/12/04 20:33:36 aspinall Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -16,12 +16,12 @@ - PRG="$(basename "$0")" - - ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)" --source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 -+. "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 - - - ## diagnostics - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]" -@@ -49,7 +49,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 diff --git a/math/isabelle/files/patch-bin-isatool b/math/isabelle/files/patch-bin-isatool deleted file mode 100644 index a536b5cf75ff..000000000000 --- a/math/isabelle/files/patch-bin-isatool +++ /dev/null @@ -1,32 +0,0 @@ ---- ./bin/isatool.orig Sun Sep 2 15:23:58 2007 -+++ ./bin/isatool Sun Sep 2 16:05:57 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: isatool,v 1.22 2005/05/17 07:58:47 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -16,12 +16,12 @@ - PRG="$(basename "$0")" - - ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)" --source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 -+. "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 - - - ## diagnostics - --function usage() -+usage() - { - echo - echo "Usage: $PRG TOOL [ARGS ...]" -@@ -49,7 +49,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 diff --git a/math/isabelle/files/patch-build b/math/isabelle/files/patch-build deleted file mode 100644 index 0d1a9733276c..000000000000 --- a/math/isabelle/files/patch-build +++ /dev/null @@ -1,32 +0,0 @@ ---- build.orig Sat Jan 12 16:44:25 2008 -+++ build Sat Jan 12 16:46:08 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: build,v 1.36 2005/12/01 17:41:46 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -23,12 +23,12 @@ - PRG="$(basename "$0")" - - ISABELLE_HOME="$(cd "$(dirname "$0")"; pwd -P)" --source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 -+. "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 - - - ## diagnostics - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS] [LOGICS ...]" -@@ -46,7 +46,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 diff --git a/math/isabelle/files/patch-etc-settings b/math/isabelle/files/patch-etc-settings index 56be18daf783..34ecb3965692 100644 --- a/math/isabelle/files/patch-etc-settings +++ b/math/isabelle/files/patch-etc-settings @@ -1,6 +1,6 @@ ---- etc/settings.orig Sat Jan 12 16:47:09 2008 -+++ etc/settings Sat Jan 12 16:56:24 2008 -@@ -16,60 +16,27 @@ +--- etc/settings.orig 2008-07-28 15:10:38.000000000 +1000 ++++ etc/settings 2008-07-28 15:22:08.000000000 +1000 +@@ -16,70 +16,36 @@ # not invent new ML system names unless you know what you are doing. # Only one of the sections below should be activated. @@ -15,7 +15,7 @@ - "/opt/polyml/$ML_PLATFORM" \ - $POLY_HOME) -ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version") --ML_OPTIONS="-H 500" +-ML_OPTIONS="-H 200" -ML_DBASE="" - -# Poly/ML 5.1 @@ -69,7 +69,18 @@ #ML_OPTIONS="-noinit" #ML_SUFFIX=".psv" #ML_PLATFORM="" -@@ -155,7 +122,7 @@ + +- + ### + ### Interactive sessions (cf. isatool tty) + ### + +-ISABELLE_LINE_EDITOR="" ++ISABELLE_LINE_EDITOR="%%LINE_EDIT%%" + [ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)" + [ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p ledit)" + +@@ -154,7 +120,7 @@ ### # Where to look for docs (multiple dirs separated by ':'). @@ -78,15 +89,29 @@ # Preferred document format ISABELLE_DOC_FORMAT=pdf -@@ -190,6 +157,7 @@ +@@ -189,6 +155,8 @@ # Proof General path, look in a variety of places ISABELLE_INTERFACE=$(choosefrom \ ++ "%%PREFIX%%/lib/xemacs/site-lisp/ProofGeneral/isar/interface" \ + "%%PREFIX%%/bin/proofgeneral" \ "$ISABELLE_HOME/contrib/ProofGeneral/isar/interface" \ "$ISABELLE_HOME/../ProofGeneral/isar/interface" \ "/usr/local/ProofGeneral/isar/interface" \ -@@ -223,26 +191,26 @@ +@@ -211,9 +179,9 @@ + ## Set HOME only for tools you have installed! + + # External provers +-E_HOME=$(choosefrom "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" "/usr/local/E" "") +-VAMPIRE_HOME=$(choosefrom "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" "/usr/local/Vampire" "") +-SPASS_HOME=$(choosefrom "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" "/usr/local/SPASS" "") ++E_HOME=$(choosefrom "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" "%%PREFIX%%/E" "") ++VAMPIRE_HOME=$(choosefrom "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" "%%PREFIX%%/Vampire" "") ++SPASS_HOME=$(choosefrom "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" "%%PREFIX%%/SPASS" "") + + # HOL4 proof objects (cf. Isabelle/src/HOL/Import) + #HOL4_PROOFS="$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs" +@@ -224,26 +192,26 @@ #SVC_MACHINE=sparc-sun-solaris # Mucke (mu-calculus model checker) @@ -119,13 +144,3 @@ # For configuring HOL/Matrix/cplex # LP_SOLVER is the default solver. It can be changed during runtime via Cplex.set_solver. -@@ -254,6 +222,6 @@ - #GLPK_PATH=glpsol - - # External provers --E_HOME=$(choosefrom "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" "/usr/local/E" "") --VAMPIRE_HOME=$(choosefrom "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" "/usr/local/Vampire" "") --SPASS_HOME=$(choosefrom "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" "/usr/local/SPASS" "") -+E_HOME=$(choosefrom "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" "%%PREFIX%%/E" "") -+VAMPIRE_HOME=$(choosefrom "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" "%%PREFIX%%/Vampire" "") -+SPASS_HOME=$(choosefrom "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" "%%PREFIX%%/SPASS" "") diff --git a/math/isabelle/files/patch-lib-Tools-browser b/math/isabelle/files/patch-lib-Tools-browser deleted file mode 100644 index a0941efa88e6..000000000000 --- a/math/isabelle/files/patch-lib-Tools-browser +++ /dev/null @@ -1,26 +0,0 @@ ---- lib/Tools/browser.orig Sat Jan 12 16:56:56 2008 -+++ lib/Tools/browser Sat Jan 12 16:58:42 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: browser,v 1.17 2006/09/18 17:12:41 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -8,7 +8,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS] [GRAPHFILE]" -@@ -20,7 +20,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 diff --git a/math/isabelle/files/patch-lib-Tools-codegen b/math/isabelle/files/patch-lib-Tools-codegen deleted file mode 100644 index 786015002556..000000000000 --- a/math/isabelle/files/patch-lib-Tools-codegen +++ /dev/null @@ -1,17 +0,0 @@ ---- lib/Tools/codegen.orig Sat Jan 12 17:19:17 2008 -+++ lib/Tools/codegen Sat Jan 12 17:19:37 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: codegen,v 1.5 2007/11/21 13:18:23 haftmann Exp $ - # Author: Florian Haftmann, TUM -@@ -10,7 +10,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG IMAGE THY SERI" diff --git a/math/isabelle/files/patch-lib-Tools-convert b/math/isabelle/files/patch-lib-Tools-convert deleted file mode 100644 index 97a0515e6ee2..000000000000 --- a/math/isabelle/files/patch-lib-Tools-convert +++ /dev/null @@ -1,17 +0,0 @@ ---- ./lib/Tools/convert.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/convert Sun Sep 2 15:48:00 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: convert,v 1.5 2005/04/26 17:50:57 wenzelm Exp $ - # Author: David von Oheimb, TU Muenchen -@@ -10,7 +10,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [FILES|DIRS...]" diff --git a/math/isabelle/files/patch-lib-Tools-dimacs2hol b/math/isabelle/files/patch-lib-Tools-dimacs2hol deleted file mode 100644 index 2cff3a23e8a1..000000000000 --- a/math/isabelle/files/patch-lib-Tools-dimacs2hol +++ /dev/null @@ -1,17 +0,0 @@ ---- ./lib/Tools/dimacs2hol.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/dimacs2hol Sun Sep 2 15:48:05 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: dimacs2hol,v 1.3 2005/04/26 17:50:57 wenzelm Exp $ - # Author: Tjark Weber -@@ -11,7 +11,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG FILES" diff --git a/math/isabelle/files/patch-lib-Tools-display b/math/isabelle/files/patch-lib-Tools-display deleted file mode 100644 index beebd48dc0f7..000000000000 --- a/math/isabelle/files/patch-lib-Tools-display +++ /dev/null @@ -1,26 +0,0 @@ ---- lib/Tools/display.orig Sat Jan 12 16:57:02 2008 -+++ lib/Tools/display Sat Jan 12 17:00:11 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: display,v 1.10 2006/11/13 17:19:24 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -8,7 +8,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS] FILE" -@@ -21,7 +21,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 diff --git a/math/isabelle/files/patch-lib-Tools-doc b/math/isabelle/files/patch-lib-Tools-doc deleted file mode 100644 index 47790edec2c6..000000000000 --- a/math/isabelle/files/patch-lib-Tools-doc +++ /dev/null @@ -1,26 +0,0 @@ ---- ./lib/Tools/doc.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/doc Sun Sep 2 15:48:14 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: doc,v 1.13 2005/04/13 16:48:06 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -8,7 +8,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [DOC]" -@@ -18,7 +18,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 diff --git a/math/isabelle/files/patch-lib-Tools-document b/math/isabelle/files/patch-lib-Tools-document deleted file mode 100644 index f2553f4c41ee..000000000000 --- a/math/isabelle/files/patch-lib-Tools-document +++ /dev/null @@ -1,44 +0,0 @@ ---- ./lib/Tools/document.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/document Sun Sep 2 15:48:20 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: document,v 1.22 2005/08/16 11:42:15 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -8,7 +8,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS] [DIR]" -@@ -25,7 +25,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 -@@ -88,7 +88,7 @@ - - # tagged region markup - --function prep_tags () -+prep_tags () - { - ( - IFS="," -@@ -115,7 +115,7 @@ - - # prepare document - --function pre_latex () -+pre_latex () - { - local FMT="$1" - [ -n "$CLEAN" ] && rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log diff --git a/math/isabelle/files/patch-lib-Tools-expandshort b/math/isabelle/files/patch-lib-Tools-expandshort deleted file mode 100644 index d8f622317fa2..000000000000 --- a/math/isabelle/files/patch-lib-Tools-expandshort +++ /dev/null @@ -1,17 +0,0 @@ ---- ./lib/Tools/expandshort.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/expandshort Sun Sep 2 15:48:24 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: expandshort,v 1.15 2005/04/26 17:50:57 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -8,7 +8,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [FILES|DIRS...]" diff --git a/math/isabelle/files/patch-lib-Tools-findlogics b/math/isabelle/files/patch-lib-Tools-findlogics deleted file mode 100644 index e992cb876e60..000000000000 --- a/math/isabelle/files/patch-lib-Tools-findlogics +++ /dev/null @@ -1,17 +0,0 @@ ---- lib/Tools/findlogics.orig Sat Jan 12 16:57:07 2008 -+++ lib/Tools/findlogics Sat Jan 12 17:00:42 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: findlogics,v 1.9 2005/10/08 18:15:31 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -8,7 +8,7 @@ - - PRG=$(basename "$0") - --function usage() -+usage() - { - echo - echo "Usage: $PRG" diff --git a/math/isabelle/files/patch-lib-Tools-fixcpure b/math/isabelle/files/patch-lib-Tools-fixcpure deleted file mode 100644 index 987dee280477..000000000000 --- a/math/isabelle/files/patch-lib-Tools-fixcpure +++ /dev/null @@ -1,17 +0,0 @@ ---- ./lib/Tools/fixcpure.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/fixcpure Sun Sep 2 15:48:31 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: fixcpure,v 1.2 2005/04/26 17:50:57 wenzelm Exp $ - # Author: Makarius -@@ -10,7 +10,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [FILES|DIRS...]" diff --git a/math/isabelle/files/patch-lib-Tools-fixgreek b/math/isabelle/files/patch-lib-Tools-fixgreek deleted file mode 100644 index d182ad0a897e..000000000000 --- a/math/isabelle/files/patch-lib-Tools-fixgreek +++ /dev/null @@ -1,17 +0,0 @@ ---- ./lib/Tools/fixgreek.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/fixgreek Sun Sep 2 15:48:35 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: fixgreek,v 1.4 2005/04/26 17:50:58 wenzelm Exp $ - # Author: Sebastian Skalberg, TU Muenchen -@@ -10,7 +10,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [FILES|DIRS...]" diff --git a/math/isabelle/files/patch-lib-Tools-fixheaders b/math/isabelle/files/patch-lib-Tools-fixheaders deleted file mode 100644 index a73ea7a9bb17..000000000000 --- a/math/isabelle/files/patch-lib-Tools-fixheaders +++ /dev/null @@ -1,17 +0,0 @@ ---- ./lib/Tools/fixheaders.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/fixheaders Sun Sep 2 15:48:38 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: fixheaders,v 1.2 2005/07/06 08:34:07 wenzelm Exp $ - # Author: Florian Haftmann, TUM -@@ -10,7 +10,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [FILES|DIRS...]" diff --git a/math/isabelle/files/patch-lib-Tools-fixsome b/math/isabelle/files/patch-lib-Tools-fixsome deleted file mode 100644 index 6af6a93a2f3e..000000000000 --- a/math/isabelle/files/patch-lib-Tools-fixsome +++ /dev/null @@ -1,17 +0,0 @@ ---- ./lib/Tools/fixsome.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/fixsome Sun Sep 2 15:48:42 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: fixsome,v 1.7 2005/04/26 17:50:58 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -10,7 +10,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [FILES|DIRS...]" diff --git a/math/isabelle/files/patch-lib-Tools-getenv b/math/isabelle/files/patch-lib-Tools-getenv deleted file mode 100644 index 310071e543ed..000000000000 --- a/math/isabelle/files/patch-lib-Tools-getenv +++ /dev/null @@ -1,17 +0,0 @@ ---- ./lib/Tools/getenv.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/getenv Sun Sep 2 15:48:46 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: getenv,v 1.11 2005/09/01 20:49:18 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -10,7 +10,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS] [VARNAMES ...]" diff --git a/math/isabelle/files/patch-lib-Tools-install b/math/isabelle/files/patch-lib-Tools-install deleted file mode 100644 index 8c61bcea857e..000000000000 --- a/math/isabelle/files/patch-lib-Tools-install +++ /dev/null @@ -1,54 +0,0 @@ ---- ./lib/Tools/install.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/install Sun Sep 2 15:52:30 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: install,v 1.25 2005/07/01 12:41:57 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -8,7 +8,7 @@ - - PRG=$(basename "$0") - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS]" -@@ -24,7 +24,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 -@@ -71,18 +71,6 @@ - - # standalone binaries - --#set by configure --AUTO_BASH=bash -- --case "$AUTO_BASH" in -- /*) -- BASH="$AUTO_BASH" -- ;; -- *) -- BASH="/usr/bin/env bash" -- ;; --esac -- - if [ -n "$BINDIR" ]; then - mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR" - -@@ -92,7 +80,7 @@ - DIST="$DISTDIR/bin/$NAME" - echo "installing $BIN" - rm -f "$BIN" -- echo "#!$BASH" > "$BIN" || fail "Cannot write file: $BIN" -+ echo "#!/bin/sh" > "$BIN" || fail "Cannot write file: $BIN" - echo >> "$BIN" - echo "exec \"$DIST\" \"\$@\"" >> "$BIN" - chmod +x "$BIN" diff --git a/math/isabelle/files/patch-lib-Tools-keywords b/math/isabelle/files/patch-lib-Tools-keywords deleted file mode 100644 index 95494253e834..000000000000 --- a/math/isabelle/files/patch-lib-Tools-keywords +++ /dev/null @@ -1,17 +0,0 @@ ---- lib/Tools/keywords.orig Sat Jan 12 17:16:34 2008 -+++ lib/Tools/keywords Sat Jan 12 17:17:21 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: keywords,v 1.3 2007/10/07 11:32:15 wenzelm Exp $ - # Author: Makarius -@@ -10,7 +10,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS] [LOGS ...]" diff --git a/math/isabelle/files/patch-lib-Tools-latex b/math/isabelle/files/patch-lib-Tools-latex deleted file mode 100644 index 8c4881b113f8..000000000000 --- a/math/isabelle/files/patch-lib-Tools-latex +++ /dev/null @@ -1,65 +0,0 @@ ---- ./lib/Tools/latex.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/latex Sun Sep 2 15:48:54 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: latex,v 1.27 2005/07/19 15:21:45 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -8,7 +8,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS] [FILE]" -@@ -23,7 +23,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 -@@ -67,7 +67,7 @@ - FILEBASE=$(basename "$FILE" .tex) - [ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE" - --function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; } -+check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; } - - - # operations -@@ -75,13 +75,13 @@ - #set by configure - AUTO_PERL=perl - --function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } --function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } --function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; } --function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; } --function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; } --function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; } --function copy_styles () -+run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } -+run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } -+run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; } -+run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; } -+run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; } -+run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; } -+copy_styles () - { - for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty - do -@@ -90,7 +90,7 @@ - done - } - --function extract_syms () -+extract_syms () - { - "$AUTO_PERL" -n \ - -e '(!m,%requires, || m,%requires latin1, || m,%requires amssymb, || m,%requires textcomp,) && m,\\newcommand\{\\isasym(\w+)\}, && print "$1\n";' \ diff --git a/math/isabelle/files/patch-lib-Tools-logo b/math/isabelle/files/patch-lib-Tools-logo deleted file mode 100644 index 96d4abb02507..000000000000 --- a/math/isabelle/files/patch-lib-Tools-logo +++ /dev/null @@ -1,26 +0,0 @@ ---- ./lib/Tools/logo.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/logo Sun Sep 2 15:49:00 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: logo,v 1.10 2005/04/26 17:50:58 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -8,7 +8,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS] NAME" -@@ -22,7 +22,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 diff --git a/math/isabelle/files/patch-lib-Tools-make b/math/isabelle/files/patch-lib-Tools-make deleted file mode 100644 index 38124254928e..000000000000 --- a/math/isabelle/files/patch-lib-Tools-make +++ /dev/null @@ -1,17 +0,0 @@ ---- ./lib/Tools/make.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/make Sun Sep 2 15:49:08 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: make,v 1.9 2004/06/21 08:25:57 kleing Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -8,7 +8,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [ARGS ...]" diff --git a/math/isabelle/files/patch-lib-Tools-makeall b/math/isabelle/files/patch-lib-Tools-makeall deleted file mode 100644 index 01a5e28d69eb..000000000000 --- a/math/isabelle/files/patch-lib-Tools-makeall +++ /dev/null @@ -1,26 +0,0 @@ ---- lib/Tools/makeall.orig Sat Jan 12 16:57:16 2008 -+++ lib/Tools/makeall Sat Jan 12 17:01:23 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: makeall,v 1.20 2005/12/01 17:41:46 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -14,7 +14,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [ARGS ...]" -@@ -24,7 +24,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 diff --git a/math/isabelle/files/patch-lib-Tools-mkdir b/math/isabelle/files/patch-lib-Tools-mkdir deleted file mode 100644 index f4c113000e98..000000000000 --- a/math/isabelle/files/patch-lib-Tools-mkdir +++ /dev/null @@ -1,26 +0,0 @@ ---- lib/Tools/mkdir.orig Sat Jan 12 16:57:23 2008 -+++ lib/Tools/mkdir Sat Jan 12 17:02:14 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: mkdir,v 1.45 2007/11/12 10:18:51 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -10,7 +10,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS] [LOGIC] NAME" -@@ -27,7 +27,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 diff --git a/math/isabelle/files/patch-lib-Tools-mkproject b/math/isabelle/files/patch-lib-Tools-mkproject deleted file mode 100644 index 069af7d50cb9..000000000000 --- a/math/isabelle/files/patch-lib-Tools-mkproject +++ /dev/null @@ -1,17 +0,0 @@ ---- lib/Tools/mkproject.orig Sat Jan 12 17:18:15 2008 -+++ lib/Tools/mkproject Sat Jan 12 17:18:41 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: mkproject,v 1.2 2007/08/09 17:19:23 wenzelm Exp $ - # Author: David Aspinall and Makarius Wenzel -@@ -7,7 +7,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG NAME" diff --git a/math/isabelle/files/patch-lib-Tools-print b/math/isabelle/files/patch-lib-Tools-print deleted file mode 100644 index b64170ce1ee6..000000000000 --- a/math/isabelle/files/patch-lib-Tools-print +++ /dev/null @@ -1,26 +0,0 @@ ---- ./lib/Tools/print.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/print Sun Sep 2 15:49:21 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: print,v 1.2 2004/06/29 09:21:18 kleing Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -8,7 +8,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS] FILE" -@@ -21,7 +21,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 diff --git a/math/isabelle/files/patch-lib-Tools-unsymbolize b/math/isabelle/files/patch-lib-Tools-unsymbolize deleted file mode 100644 index 35a0665b887a..000000000000 --- a/math/isabelle/files/patch-lib-Tools-unsymbolize +++ /dev/null @@ -1,17 +0,0 @@ ---- ./lib/Tools/unsymbolize.orig Sun Sep 2 15:11:55 2007 -+++ ./lib/Tools/unsymbolize Sun Sep 2 15:49:24 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: unsymbolize,v 1.6 2005/04/26 17:50:58 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -10,7 +10,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [FILES|DIRS...]" diff --git a/math/isabelle/files/patch-lib-Tools-usedir b/math/isabelle/files/patch-lib-Tools-usedir deleted file mode 100644 index 219da65abdcf..000000000000 --- a/math/isabelle/files/patch-lib-Tools-usedir +++ /dev/null @@ -1,48 +0,0 @@ ---- lib/Tools/usedir.orig Sat Jan 12 16:57:29 2008 -+++ lib/Tools/usedir Sat Jan 12 17:03:34 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: usedir,v 1.67 2007/10/30 09:52:26 haftmann Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -10,7 +10,7 @@ - - PRG="$(basename "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS] LOGIC NAME" -@@ -43,18 +43,18 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 - } - --function check_bool() -+check_bool() - { - [ "$1" = true -o "$1" = false ] || fail "Bad boolean: \"$1\"" - } - --function check_number() -+check_number() - { - [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\"" - } -@@ -82,7 +82,7 @@ - PROOFS=0 - VERBOSE=false - --function getoptions() -+getoptions() - { - OPTIND=1 - while getopts "C:D:M:P:T:V:bc:d:f:g:i:m:p:rs:v:" OPT diff --git a/math/isabelle/files/patch-lib-Tools-version b/math/isabelle/files/patch-lib-Tools-version deleted file mode 100644 index 0e7a6c9fc596..000000000000 --- a/math/isabelle/files/patch-lib-Tools-version +++ /dev/null @@ -1,8 +0,0 @@ ---- lib/Tools/version.orig Sat Jan 12 16:57:34 2008 -+++ lib/Tools/version Sat Jan 12 17:03:48 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: version,v 1.2 2004/06/21 08:25:57 kleing Exp $ - # Author: Stefan Berghofer, TU Muenchen diff --git a/math/isabelle/files/patch-lib-scripts-configure b/math/isabelle/files/patch-lib-scripts-configure deleted file mode 100644 index 60bab756414c..000000000000 --- a/math/isabelle/files/patch-lib-scripts-configure +++ /dev/null @@ -1,15 +0,0 @@ ---- lib/scripts/configure.orig Fri Sep 14 18:00:10 2007 -+++ lib/scripts/configure Fri Sep 14 18:00:21 2007 -@@ -8,11 +8,5 @@ - ## patch scripts - - cd "`dirname "$0"`" -+exec sh lib/scripts/patch-scripts.bash - --if bash -c : --then -- bash lib/scripts/patch-scripts.bash --else -- echo "FATAL ERROR: bash not found!" -- exit 2 --fi diff --git a/math/isabelle/files/patch-lib-scripts-feeder b/math/isabelle/files/patch-lib-scripts-feeder deleted file mode 100644 index 2c0963651e3a..000000000000 --- a/math/isabelle/files/patch-lib-scripts-feeder +++ /dev/null @@ -1,26 +0,0 @@ ---- ./lib/scripts/feeder.orig Sun Sep 2 15:12:50 2007 -+++ ./lib/scripts/feeder Sun Sep 2 15:54:12 2007 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: feeder,v 1.10 2005/04/26 17:50:58 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -11,7 +11,7 @@ - PRG="$(basename "$0")" - DIR="$(dirname "$0")" - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS]" -@@ -27,7 +27,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 diff --git a/math/isabelle/files/patch-lib-scripts-fileindent b/math/isabelle/files/patch-lib-scripts-fileindent deleted file mode 100644 index 39a7d8624656..000000000000 --- a/math/isabelle/files/patch-lib-scripts-fileindent +++ /dev/null @@ -1,8 +0,0 @@ ---- lib/scripts/fileident.orig Sat Jan 12 17:20:26 2008 -+++ lib/scripts/fileident Sat Jan 12 17:20:38 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: fileident,v 1.1 2007/07/17 20:51:27 wenzelm Exp $ - # diff --git a/math/isabelle/files/patch-lib-scripts-getsettings b/math/isabelle/files/patch-lib-scripts-getsettings deleted file mode 100644 index 49fea452c414..000000000000 --- a/math/isabelle/files/patch-lib-scripts-getsettings +++ /dev/null @@ -1,30 +0,0 @@ ---- lib/scripts/getsettings.orig Sat Jan 12 17:08:58 2008 -+++ lib/scripts/getsettings Sat Jan 12 17:10:17 2008 -@@ -27,10 +27,9 @@ - - #users tend to put strange things in here ... - unset ENV --unset BASH_ENV - - #support easy settings --function choosefrom () -+choosefrom () - { - local RESULT="" - local FILE="" -@@ -45,13 +44,13 @@ - } - - #get actual settings --source "$ISABELLE_HOME/etc/settings" || exit 2 -+. "$ISABELLE_HOME/etc/settings" || exit 2 - ISABELLE_SITE_SETTINGS_PRESENT=true - - [ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \ - { echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER should not be the same directory!"; } - [ -z "$ISABELLE_IGNORE_USER_SETTINGS" -a -f "$ISABELLE_HOME_USER/etc/settings" ] && \ -- { source "$ISABELLE_HOME_USER/etc/settings" || exit 2; } -+ { . "$ISABELLE_HOME_USER/etc/settings" || exit 2; } - - #ML system identifier - if [ -z "$ML_PLATFORM" ]; then diff --git a/math/isabelle/files/patch-lib-scripts-patch_scripts.bash b/math/isabelle/files/patch-lib-scripts-patch_scripts.bash deleted file mode 100644 index 712f12891bac..000000000000 --- a/math/isabelle/files/patch-lib-scripts-patch_scripts.bash +++ /dev/null @@ -1,37 +0,0 @@ ---- lib/scripts/patch-scripts.bash.orig Sun Sep 2 15:55:18 2007 -+++ lib/scripts/patch-scripts.bash Sun Sep 2 16:06:41 2007 -@@ -3,12 +3,12 @@ - # Author: Markus Wenzel, TU Muenchen - # - # patch-scripts.bash - relocate interpreter paths of executable scripts and --# insert AUTO_BASH/AUTO_PERL values -+# insert AUTO_PERL values - # - - ## find binaries - --function findbin() -+findbin() - { - local BASE="$1" - local BINARY="" -@@ -29,17 +29,14 @@ - - ## main - --[ -z "$BASH_PATH" ] && BASH_PATH=$(findbin bash) - [ -z "$PERL_PATH" ] && PERL_PATH=$(findbin perl) --[ -z "$AUTO_BASH" ] && AUTO_BASH="$BASH_PATH" - [ -z "$AUTO_PERL" ] && AUTO_PERL="$PERL_PATH" - - for FILE in $(find . -type f -print) - do - if [ -x "$FILE" ]; then -- sed -e "s:^#!.*/bash:#!$BASH_PATH:" -e "s:^#!.*/perl:#!$PERL_PATH:" \ -- -e "s:^AUTO_BASH=.*bash:AUTO_BASH=$AUTO_BASH:" \ -- -e "s:^AUTO_PERL=.*perl:AUTO_PERL=$AUTO_PERL:" "$FILE" > "$FILE~~" -+ sed -e "s:^#!.*/perl:#!$PERL_PATH:" \ -+ -e "s:^AUTO_PERL=.*perl:AUTO_PERL=$AUTO_PERL:" "$FILE" > "$FILE~~" - if cmp -s "$FILE" "$FILE~~"; then - rm "$FILE~~" - else diff --git a/math/isabelle/files/patch-lib-scripts-polyml_platform b/math/isabelle/files/patch-lib-scripts-polyml_platform deleted file mode 100644 index 911d496b6a1f..000000000000 --- a/math/isabelle/files/patch-lib-scripts-polyml_platform +++ /dev/null @@ -1,8 +0,0 @@ ---- lib/scripts/polyml-platform.orig Sat Jan 12 17:09:07 2008 -+++ lib/scripts/polyml-platform Sat Jan 12 17:11:51 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: polyml-platform,v 1.6 2007/11/08 19:07:58 wenzelm Exp $ - # diff --git a/math/isabelle/files/patch-lib-scripts-polyml_version b/math/isabelle/files/patch-lib-scripts-polyml_version deleted file mode 100644 index cd6be76c2ecd..000000000000 --- a/math/isabelle/files/patch-lib-scripts-polyml_version +++ /dev/null @@ -1,8 +0,0 @@ ---- lib/scripts/polyml-version.orig Sat Jan 12 17:09:13 2008 -+++ lib/scripts/polyml-version Sat Jan 12 17:15:41 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: polyml-version,v 1.5 2006/12/05 17:32:54 wenzelm Exp $ - # diff --git a/math/isabelle/files/patch-lib-scripts-run_mosml b/math/isabelle/files/patch-lib-scripts-run_mosml deleted file mode 100644 index bc7fa92d97af..000000000000 --- a/math/isabelle/files/patch-lib-scripts-run_mosml +++ /dev/null @@ -1,35 +0,0 @@ ---- lib/scripts/run-mosml.orig Mon Jun 21 18:25:58 2004 -+++ lib/scripts/run-mosml Sun Sep 2 17:14:13 2007 -@@ -1,16 +1,14 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: run-mosml,v 1.8 2004/06/21 08:25:58 kleing Exp $ - # Author: Markus Wenzel, TU Muenchen - # - # Moscow ML 2.00 startup script - --export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE -- - - ## diagnostics - --function fail_out() -+fail_out() - { - echo "Unable to create output heap file: \"$OUTFILE\"" >&2 - exit 2 -@@ -37,6 +35,13 @@ - [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } - fi - -+SAVE_OUTFILE="$OUTFILE" -+SAVE_MLTEXT="$MLTEXT" -+SAVE_NOWRITE="$NOWRITE" -+unset INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE -+OUTFILE="$SAVE_OUTFILE" -+MLTEXT="$SAVE_MLTEXT" -+NOWRITE="$SAVE_NOWRITE" - - ## run it! - diff --git a/math/isabelle/files/patch-lib-scripts-run_polyml b/math/isabelle/files/patch-lib-scripts-run_polyml deleted file mode 100644 index f2ae5e4a57a2..000000000000 --- a/math/isabelle/files/patch-lib-scripts-run_polyml +++ /dev/null @@ -1,45 +0,0 @@ ---- lib/scripts/run-polyml.orig Sun Oct 21 04:31:50 2007 -+++ lib/scripts/run-polyml Sat Jan 12 18:01:17 2008 -@@ -5,18 +5,15 @@ - # - # Poly/ML startup script. - --export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE -- -- - ## diagnostics - --function fail_out() -+fail_out() - { - echo "Unable to create output heap file: \"$OUTFILE\"" >&2 - exit 2 - } - --function check_file() -+check_file() - { - if [ ! -f "$1" ]; then - echo "Unable to locate $1" >&2 -@@ -25,6 +22,21 @@ - fi - } - -+SAVE_INFILE="$INFILE" -+SAVE_OUTFILE="$OUTFILE" -+SAVE_COPYDB="$COPYDB" -+SAVE_COMPRESS="$COMPRESS" -+SAVE_MLTEXT="$MLTEXT" -+SAVE_TERMINATE="$TERMINATE" -+SAVE_NOWRITE="$NOWRITE" -+unset INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE -+INFILE="$SAVE_INFILE" -+OUTFILE="$SAVE_OUTFILE" -+COPYDB="$SAVE_COPYDB" -+COMPRESS="$SAVE_COMPRESS" -+MLTEXT="$SAVE_MLTEXT" -+TERMINATE="$SAVE_TERMINATE" -+NOWRITE="$SAVE_NOWRITE" - - ## Poly/ML executable and database - diff --git a/math/isabelle/files/patch-lib-scripts-run_polyml_5.0 b/math/isabelle/files/patch-lib-scripts-run_polyml_5.0 deleted file mode 100644 index 4ece1175bd54..000000000000 --- a/math/isabelle/files/patch-lib-scripts-run_polyml_5.0 +++ /dev/null @@ -1,50 +0,0 @@ ---- lib/scripts/run-polyml-5.0.orig Sun Oct 21 04:32:23 2007 -+++ lib/scripts/run-polyml-5.0 Sat Jan 12 18:01:28 2008 -@@ -1,22 +1,20 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: run-polyml-5.0,v 1.9 2007/10/20 18:32:23 wenzelm Exp $ - # Author: Makarius - # - # Poly/ML startup script (for 5.0) - --export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE -- - - ## diagnostics - --function fail_out() -+fail_out() - { - echo "Unable to create output heap file: \"$OUTFILE\"" >&2 - exit 2 - } - --function check_file() -+check_file() - { - if [ ! -f "$1" ]; then - echo "Unable to locate $1" >&2 -@@ -25,6 +23,21 @@ - fi - } - -+SAVE_INFILE="$INFILE" -+SAVE_OUTFILE="$OUTFILE" -+SAVE_COPYDB="$COPYDB" -+SAVE_COMPRESS="$COMPRESS" -+SAVE_MLTEXT="$MLTEXT" -+SAVE_TERMINATE="$TERMINATE" -+SAVE_NOWRITE="$NOWRITE" -+unset INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE -+INFILE="$SAVE_INFILE" -+OUTFILE="$SAVE_OUTFILE" -+COPYDB="$SAVE_COPYDB" -+COMPRESS="$SAVE_COMPRESS" -+MLTEXT="$SAVE_MLTEXT" -+TERMINATE="$SAVE_TERMINATE" -+NOWRITE="$SAVE_NOWRITE" - - ## compiler executables and libraries - diff --git a/math/isabelle/files/patch-lib-scripts-run_polyml_5.1 b/math/isabelle/files/patch-lib-scripts-run_polyml_5.1 deleted file mode 100644 index 212bf2b467fa..000000000000 --- a/math/isabelle/files/patch-lib-scripts-run_polyml_5.1 +++ /dev/null @@ -1,50 +0,0 @@ ---- lib/scripts/run-polyml-5.1.orig Tue Nov 20 21:42:15 2007 -+++ lib/scripts/run-polyml-5.1 Sat Jan 12 18:01:39 2008 -@@ -1,22 +1,20 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: run-polyml-5.1,v 1.7 2007/11/20 10:42:15 wenzelm Exp $ - # Author: Makarius - # - # Poly/ML startup script (for 5.1) - --export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE -- - - ## diagnostics - --function fail_out() -+fail_out() - { - echo "Unable to create output heap file: \"$OUTFILE\"" >&2 - exit 2 - } - --function check_file() -+check_file() - { - if [ ! -f "$1" ]; then - echo "Unable to locate $1" >&2 -@@ -25,6 +23,21 @@ - fi - } - -+SAVE_INFILE="$INFILE" -+SAVE_OUTFILE="$OUTFILE" -+SAVE_COPYDB="$COPYDB" -+SAVE_COMPRESS="$COMPRESS" -+SAVE_MLTEXT="$MLTEXT" -+SAVE_TERMINATE="$TERMINATE" -+SAVE_NOWRITE="$NOWRITE" -+unset INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE -+INFILE="$SAVE_INFILE" -+OUTFILE="$SAVE_OUTFILE" -+COPYDB="$SAVE_COPYDB" -+COMPRESS="$SAVE_COMPRESS" -+MLTEXT="$SAVE_MLTEXT" -+TERMINATE="$SAVE_TERMINATE" -+NOWRITE="$SAVE_NOWRITE" - - ## compiler executables and libraries - diff --git a/math/isabelle/files/patch-lib-scripts-run_poplogml b/math/isabelle/files/patch-lib-scripts-run_poplogml deleted file mode 100644 index f0a27abc35f9..000000000000 --- a/math/isabelle/files/patch-lib-scripts-run_poplogml +++ /dev/null @@ -1,59 +0,0 @@ ---- lib/scripts/run-poplogml.orig Tue Oct 11 21:28:04 2005 -+++ lib/scripts/run-poplogml Sat Jan 12 18:01:54 2008 -@@ -1,22 +1,20 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: run-poplogml,v 1.5 2005/10/11 11:28:04 wenzelm Exp $ - # Author: Makarius - # - # Poplog/PML startup script (version 15.6/2.1). - --export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE -- - - ## diagnostics - --function fail_out() -+fail_out() - { - echo "Unable to create output heap file: \"$OUTFILE\"" >&2 - exit 2 - } - --function check_mlhome_file() -+check_mlhome_file() - { - if [ ! -f "$1" ]; then - echo "Unable to locate $1" >&2 -@@ -25,7 +23,7 @@ - fi - } - --function check_heap_file() -+check_heap_file() - { - if [ ! -f "$1" ]; then - echo "Expected to find ML heap file $1" >&2 -@@ -35,6 +33,21 @@ - fi - } - -+SAVE_INFILE="$INFILE" -+SAVE_OUTFILE="$OUTFILE" -+SAVE_COPYDB="$COPYDB" -+SAVE_COMPRESS="$COMPRESS" -+SAVE_MLTEXT="$MLTEXT" -+SAVE_TERMINATE="$TERMINATE" -+SAVE_NOWRITE="$NOWRITE" -+unset INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE -+INFILE="$SAVE_INFILE" -+OUTFILE="$SAVE_OUTFILE" -+COPYDB="$SAVE_COPYDB" -+COMPRESS="$SAVE_COMPRESS" -+MLTEXT="$SAVE_MLTEXT" -+TERMINATE="$SAVE_TERMINATE" -+NOWRITE="$SAVE_NOWRITE" - - ## prepare databases - diff --git a/math/isabelle/files/patch-lib-scripts-run_smlnj b/math/isabelle/files/patch-lib-scripts-run_smlnj index 5d3b82fedbbf..687fb62bacaa 100644 --- a/math/isabelle/files/patch-lib-scripts-run_smlnj +++ b/math/isabelle/files/patch-lib-scripts-run_smlnj @@ -1,43 +1,10 @@ ---- lib/scripts/run-smlnj.orig Mon Jun 21 18:25:58 2004 -+++ lib/scripts/run-smlnj Fri Sep 14 18:01:25 2007 -@@ -1,22 +1,20 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: run-smlnj,v 1.28 2004/06/21 08:25:58 kleing Exp $ - # Author: Markus Wenzel, TU Muenchen - # - # SML/NJ startup script (for 110 or later). +--- lib/scripts/run-smlnj.orig 2004-06-21 18:25:58.000000000 +1000 ++++ lib/scripts/run-smlnj 2008-07-29 15:49:30.000000000 +1000 +@@ -39,11 +39,10 @@ --export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE -- - - ## diagnostics - --function fail_out() -+fail_out() - { - echo "Unable to create output heap file: \"$OUTFILE\"" >&2 - exit 2 - } - --function check_mlhome_file() -+check_mlhome_file() - { - if [ ! -f "$1" ]; then - echo "Unable to locate $1" >&2 -@@ -25,7 +23,7 @@ - fi - } - --function check_heap_file() -+check_heap_file() - { - if [ ! -f "$1" ]; then - echo "Expected to find ML heap file $1" >&2 -@@ -40,10 +38,8 @@ ## compiler binaries ++export SMLNJ_DEVEL=yes SML="$ML_HOME/sml" -ARCH_N_OPSYS="$ML_HOME/.arch-n-opsys" @@ -46,22 +13,7 @@ -@@ -76,6 +72,14 @@ - FEEDER_OPTS="-q" - fi - -+SAVE_OUTFILE="$OUTFILE" -+SAVE_MLTEXT="$MLTEXT" -+SAVE_NOWRITE="$NOWRITE" -+unset INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE -+OUTFILE="$SAVE_OUTFILE" -+MLTEXT="$SAVE_MLTEXT" -+NOWRITE="$SAVE_NOWRITE" -+ - "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ - { read FPID; "$SML" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } - RC="$?" -@@ -84,8 +88,7 @@ +@@ -84,8 +83,7 @@ ## fix heap file name and permissions if [ -n "$OUTFILE" ]; then diff --git a/math/isabelle/files/patch-lib-scripts-timestart.bash b/math/isabelle/files/patch-lib-scripts-timestart.bash deleted file mode 100644 index bba13d73fc06..000000000000 --- a/math/isabelle/files/patch-lib-scripts-timestart.bash +++ /dev/null @@ -1,16 +0,0 @@ ---- lib/scripts/timestart.bash.orig Thu Dec 8 01:23:22 2005 -+++ lib/scripts/timestart.bash Sat Jan 12 17:53:32 2008 -@@ -10,9 +10,11 @@ - #set by configure - AUTO_PERL=perl - --function get_times () { -- local TMP="/tmp/get_times$$" -+get_times () { -+ local TMP SECONDS -+ TMP="/tmp/get_times$$" - times > "$TMP" # No pipe here! -+ SECONDS=$(( `date +'%j * 86400 + %H * 3600 + %M * 60 + %S'` )) - TIMES_RESULT="$SECONDS $(echo $(cat "$TMP") | "$AUTO_PERL" -pe 's,\d+m\d+\.\d+s \d+m\d+\.\d+s (\d+)m(\d+)\.\d+s +(\d+)m(\d+)\.\d+s, $1 * 60 + $2 + $3 * 60 + $4,e')" - rm -f "$TMP" - } diff --git a/math/isabelle/files/patch-lib-scripts-timestop.bash b/math/isabelle/files/patch-lib-scripts-timestop.bash deleted file mode 100644 index fc672fb7d325..000000000000 --- a/math/isabelle/files/patch-lib-scripts-timestop.bash +++ /dev/null @@ -1,44 +0,0 @@ ---- lib/scripts/timestop.bash.orig Fri Dec 2 04:44:47 2005 -+++ lib/scripts/timestop.bash Sat Jan 12 17:54:13 2008 -@@ -7,28 +7,29 @@ - - TIMES_REPORT="" - --function show_times () -+show_times () - { -- local TIMES_START="$TIMES_RESULT" -+ local TIMES_START TIMES_STOP KIND START STOP TIME SECS MINUTES HOURS \ -+ KIND_NAME RESULT -+ -+ TIMES_START="$TIMES_RESULT" - get_times -- local TIMES_STOP="$TIMES_RESULT" -- local KIND -+ TIMES_STOP="$TIMES_RESULT" - for KIND in 1 2 - do -- local START=$(echo "$TIMES_START" | cut -d " " -f $KIND) -- local STOP=$(echo "$TIMES_STOP" | cut -d " " -f $KIND) -+ START=$(echo "$TIMES_START" | cut -d " " -f $KIND) -+ STOP=$(echo "$TIMES_STOP" | cut -d " " -f $KIND) - -- local TIME=$[ $STOP - $START ] -- local SECS=$[ $TIME % 60 ] -+ TIME=$(( $STOP - $START )) -+ SECS=$(( $TIME % 60 )) - [ $SECS -lt 10 ] && SECS="0$SECS" -- local MINUTES=$[ ($TIME / 60) % 60 ] -+ MINUTES=$(( ($TIME / 60) % 60 )) - [ $MINUTES -lt 10 ] && MINUTES="0$MINUTES" -- local HOURS=$[ $TIME / 3600 ] -+ HOURS=$(( $TIME / 3600 )) - -- local KIND_NAME - [ "$KIND" = 1 ] && KIND_NAME="elapsed time" - [ "$KIND" = 2 ] && KIND_NAME="cpu time" -- local RESULT="${HOURS}:${MINUTES}:${SECS} ${KIND_NAME}" -+ RESULT="${HOURS}:${MINUTES}:${SECS} ${KIND_NAME}" - - if [ -z "$TIMES_REPORT" ]; then - TIMES_REPORT="$RESULT" diff --git a/math/isabelle/files/patch-src-Pure-mk b/math/isabelle/files/patch-src-Pure-mk deleted file mode 100644 index e23ecd5d35ef..000000000000 --- a/math/isabelle/files/patch-src-Pure-mk +++ /dev/null @@ -1,26 +0,0 @@ ---- src/Pure/mk.orig Sat Jan 12 17:35:00 2008 -+++ src/Pure/mk Sat Jan 12 17:36:05 2008 -@@ -1,4 +1,4 @@ --#!/usr/bin/env bash -+#!/bin/sh - # - # $Id: mk,v 1.32 2007/01/04 20:58:46 wenzelm Exp $ - # Author: Markus Wenzel, TU Muenchen -@@ -10,7 +10,7 @@ - - ## diagnostics - --function usage() -+usage() - { - echo - echo "Usage: $PRG [OPTIONS]" -@@ -23,7 +23,7 @@ - exit 1 - } - --function fail() -+fail() - { - echo "$1" >&2 - exit 2 diff --git a/math/isabelle/pkg-plist b/math/isabelle/pkg-plist index a9805936212c..f046f8b103e5 100644 --- a/math/isabelle/pkg-plist +++ b/math/isabelle/pkg-plist @@ -4,8 +4,6 @@ bin/isabelle-interface bin/isabelle-process bin/isatool %%PORTDOCS%%%%DOCSDIR%%/Contents -%%PORTDOCS%%%%DOCSDIR%%/axclass.dvi -%%PORTDOCS%%%%DOCSDIR%%/axclass.pdf %%PORTDOCS%%%%DOCSDIR%%/browser_info/CCL/.session/entries %%PORTDOCS%%%%DOCSDIR%%/browser_info/CCL/.session/pre-index %%PORTDOCS%%%%DOCSDIR%%/browser_info/CCL/CCL.html @@ -63,10 +61,8 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/CTT/isabelle.css %%PORTDOCS%%%%DOCSDIR%%/browser_info/CTT/large.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/CTT/medium.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/CTT/rew.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/CTT/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/CTT/small.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/CTT/typedsimp.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/Cube/.session/entries %%PORTDOCS%%%%DOCSDIR%%/browser_info/Cube/.session/pre-index %%PORTDOCS%%%%DOCSDIR%%/browser_info/Cube/Cube.html @@ -85,13 +81,7 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/GraphBrowser.jar %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/IFOL.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/README.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/blast.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/blastdata.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/cladata.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/clasimp.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/classical.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/document.pdf -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/eqsubst.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/ex/.session/entries %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/ex/.session/pre-index %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/ex/Classical.html @@ -120,40 +110,22 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/ex/outline.pdf %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/ex/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/ex/small.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/fologic.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/hypsubst.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/hypsubstdata.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/index.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/induct.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/intprover.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/isabelle.css -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/isand.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/large.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/medium.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/outline.pdf -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/project_rule.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/quantifier1.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/rw_inst.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/rw_tools.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/session.graph -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/simpdata.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/small.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/splitter.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/zipper.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/.session/entries %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/.session/pre-index %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/FOLP.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/FOLP_lemmas.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/GraphBrowser.jar -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/IFOLP.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/IFOLP.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/classical.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/ex/.session/entries %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/ex/.session/pre-index %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/ex/GraphBrowser.jar -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/ex/If.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/ex/If.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/ex/Nat.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/ex/Nat.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/ex/index.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/ex/isabelle.css @@ -161,20 +133,23 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/ex/medium.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/ex/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/ex/small.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/hypsubst.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/index.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/intprover.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/isabelle.css %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/large.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/medium.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/session.graph -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/simp.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/simpdata.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/small.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/ex/Classical.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/ex/Foundation.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/ex/Intro.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/ex/Intuitionistic.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/ex/Propositional_Cla.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/ex/Propositional_Int.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/ex/Quantifiers_Cla.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/ex/Quantifiers_Int.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/.session/entries %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/.session/pre-index %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ATP_Linkup.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Accessible_Part.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Arith_Tools.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Auth/.session/entries %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Auth/.session/pre-index @@ -280,7 +255,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Bali/small.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Code_Setup.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Datatype.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Dense_Linear_Order.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Divides.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Equiv_Relations.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Extraction.html @@ -355,7 +329,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/large.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/medium.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/outline.pdf -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/ringsimp.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/small.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/.session/entries @@ -367,7 +340,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Complex_Main.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ContNotDenum.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Deriv.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/EvenOdd.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Fact.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Filter.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Float.html @@ -382,32 +354,19 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/ComputeNumeral.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/Compute_Oracle.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/Cplex.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/CplexMatrixConverter.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/Cplex_tools.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/FloatSparseMatrix.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/FloatSparseMatrixBuilder.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/GraphBrowser.jar %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/LP.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/Matrix.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/MatrixGeneral.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/MatrixLP.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/MatrixLP.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/SparseMatrix.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/am.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/am_compiler.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/am_ghc.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/am_interpreter.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/am_sml.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/compute.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/document.pdf -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/fspmlp.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/index.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/isabelle.css %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/large.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/linker.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/medium.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/outline.pdf -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/report.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/small.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/.session/entries @@ -422,30 +381,16 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/HOL4Syntax.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/HOL4Vec.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/HOL4Word32.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/ImportRecorder.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/ImportRecorder.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/MakeEqual.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/Primes.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/README -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/hol4rews.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/import_package.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/import_syntax.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/index.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/isabelle.css %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/large.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/lazy_seq.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/medium.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/mono_scan.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/mono_seq.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/proof_kernel.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/replay.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/scan.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/seq.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/session.graph -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/shuffler.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/small.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/xml.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/xmlconv.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HSEQ.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HSeries.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HTranscendental.html @@ -482,29 +427,15 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/HOL4Compat.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/HOL4Setup.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/HOL4Syntax.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/ImportRecorder.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/ImportRecorder.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/MakeEqual.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/Primes.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/hol4rews.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/import_package.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/import_syntax.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/index.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/isabelle.css %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/large.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/lazy_seq.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/medium.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/mono_scan.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/mono_seq.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/proof_kernel.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/replay.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/scan.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/seq.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/session.graph -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/shuffler.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/small.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/xml.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/xmlconv.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Infinite_Set.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Integration.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Lim.html @@ -519,7 +450,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/NthRoot.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/PReal.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Parity.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Poly.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/RComplete.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/README.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Rational.html @@ -530,7 +460,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/SEQ.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Series.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Star.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/StarClasses.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/StarDef.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Taylor.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Transcendental.html @@ -563,27 +492,17 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/index.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/isabelle.css %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/large.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/linreif.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/linrtac.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/medium.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/mireif.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/mirtac.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/outline.pdf %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/small.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/float.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/float_arith.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/hypreal_arith.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/index.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/isabelle.css %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/large.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/medium.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/outline.pdf -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/rat_arith.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/real_arith.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/small.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/transfer.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/.session/entries %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/.session/pre-index %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/Examples/.session/entries @@ -602,7 +521,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/Examples/SN.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/Examples/SOS.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/Examples/Support.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/Examples/VC_Compatible.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/Examples/Weakening.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/Examples/index.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/Examples/isabelle.css @@ -617,14 +535,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/isabelle.css %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/large.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/medium.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/nominal_atoms.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/nominal_fresh_fun.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/nominal_induct.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/nominal_inductive.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/nominal_package.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/nominal_permeq.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/nominal_primrec.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/nominal_thmdecls.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/small.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Word/.session/entries @@ -686,7 +596,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Hoare/SepLogHeap.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Hoare/Separation.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Hoare/document.pdf -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Hoare/hoare_tac.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Hoare/index.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Hoare/isabelle.css %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Hoare/large.html @@ -799,8 +708,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Induct/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Induct/small.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Inductive.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/IntArith.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/IntDef.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/IntDiv.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Isar_examples/.session/entries %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Isar_examples/.session/pre-index @@ -823,7 +730,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Isar_examples/README.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Isar_examples/Summation.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Isar_examples/document.pdf -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Isar_examples/hoare_tac.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Isar_examples/index.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Isar_examples/isabelle.css %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Isar_examples/large.html @@ -833,7 +739,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Isar_examples/small.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Lambda/.session/entries %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Lambda/.session/pre-index -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Lambda/Code_Index.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Lambda/Code_Integer.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Lambda/Commutation.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Lambda/Eta.html @@ -920,7 +825,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/While_Combinator.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Word.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Zorn.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/comm_ring.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/document.pdf %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/index.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/isabelle.css @@ -1031,7 +935,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Modelcheck/isabelle.css %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Modelcheck/large.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Modelcheck/medium.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Modelcheck/mucke_oracle.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Modelcheck/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Modelcheck/small.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/NanoJava/.session/entries @@ -1087,11 +990,9 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/NumberTheory/outline.pdf %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/NumberTheory/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/NumberTheory/small.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Numeral.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/OrderedGroup.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Orderings.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Power.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/PreList.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Predicate.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Presburger.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Product_Type.html @@ -1107,7 +1008,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Prolog/isabelle.css %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Prolog/large.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Prolog/medium.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Prolog/prolog.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Prolog/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Prolog/small.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/README.html @@ -1158,7 +1058,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/SizeChange/large.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/SizeChange/medium.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/SizeChange/outline.pdf -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/SizeChange/sct.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/SizeChange/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/SizeChange/small.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Statespace/.session/entries @@ -1169,7 +1068,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Statespace/StateSpaceEx.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Statespace/StateSpaceLocale.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Statespace/StateSpaceSyntax.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Statespace/distinct_tree_prover.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Statespace/document.pdf %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Statespace/index.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Statespace/isabelle.css @@ -1178,8 +1076,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Statespace/outline.pdf %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Statespace/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Statespace/small.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Statespace/state_fun.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Statespace/state_space.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Subst/.session/entries %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Subst/.session/pre-index %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Subst/AList.html @@ -1297,7 +1193,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/UNITY/Transformers.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/UNITY/UNITY.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/UNITY/UNITY_Main.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/UNITY/UNITY_tactics.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/UNITY/Union.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/UNITY/WFair.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/UNITY/document.pdf @@ -1335,8 +1230,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/W0/outline.pdf %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/W0/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/W0/small.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Wellfounded_Recursion.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Wellfounded_Relations.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ZF/.session/entries %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ZF/.session/pre-index %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ZF/Games.html @@ -1355,40 +1248,7 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ZF/outline.pdf %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ZF/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ZF/small.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/abel_cancel.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/arith_data.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/assoc_fold.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/auto_term.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/blast.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/cancel_div_mod.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/cancel_numeral_factor.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/cancel_numerals.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/cancel_sums.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/casesplit.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/clasimp.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/classical.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/cnf_funcs.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/code_funcgr.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/code_name.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/code_package.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/code_target.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/code_thingol.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/combine_numerals.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/context_tree.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/cooper.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/cooper_data.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/datatype_abs_proofs.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/datatype_aux.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/datatype_case.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/datatype_codegen.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/datatype_package.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/datatype_prop.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/datatype_realizer.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/datatype_rep_proofs.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/dcterm.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/document.pdf -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/dseq.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/eqsubst.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/.session/entries %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/.session/pre-index %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Abstract_NAT.html @@ -1404,7 +1264,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/CTL.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Chinese.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Classical.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Classpackage.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Code_Index.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Code_Integer.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Code_Message.html @@ -1418,7 +1277,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Eval.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Eval_Examples.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/ExecutableContent.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Executable_Set.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/FuncSet.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Fundefs.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/GCD.html @@ -1443,7 +1301,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/MonoidGroup.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Multiquote.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Multiset.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/NBE.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/NatPair.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/NatSum.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Nat_Infinity.html @@ -1457,7 +1314,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Primes.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Primrec.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Product_ord.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Pure_term.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Puzzle.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Quickcheck_Examples.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/README.html @@ -1467,7 +1323,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Recdefs.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Records.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Reflected_Presburger.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Reflection.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Reflection.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Refute_Examples.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/SAT_Examples.html @@ -1480,112 +1335,59 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Unification.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/While_Combinator.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Word.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/comm_ring.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/coopereif.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/coopertac.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/document.pdf %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/index.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/isabelle.css %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/large.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/medium.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/outline.pdf -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/rat_arith.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/real_arith.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/reflection_data.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/set.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/small.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/svc_funcs.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/extract_common_term.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/fast_lin_arith.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ferrante_rackoff.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ferrante_rackoff_data.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/fundef_common.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/fundef_core.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/fundef_datatype.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/fundef_lib.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/fundef_package.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/generated_cooper.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/groebner.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/hologic.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/hypsubst.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Code_Char.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Dense_Linear_Order.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Efficient_Nat_examples.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Enum.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Induction_Scheme.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Option_ord.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Quickcheck.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/RType.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Extraction/Parity.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/Parity.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Dense_Linear_Order.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Fundamental_Theorem_Algebra.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Order_Relation.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Univ_Poly.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/Examples/Contexts.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/Examples/VC_Condition.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Isar_examples/Parity.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Array.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Countable.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Dense_Linear_Order.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Enum.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Eval.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Heap.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Heap_Monad.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Imperative_HOL.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/ListVector.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Option_ord.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Order_Relation.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/RBT.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Ref.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/RType.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Sublist_Order.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Univ_Poly.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MetisExamples/Dense_Linear_Order.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/NumberTheory/Parity.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Int.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Wellfounded.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/index.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/induct.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/inductive_codegen.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/inductive_package.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/inductive_realizer.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/inductive_set_package.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/inductive_wrap.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/int_arith1.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/int_factor_simprocs.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/isabelle.css -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/isand.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/langford.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/langford_data.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/large.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/lexicographic_order.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/lin_arith.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/medium.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/meson.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/metis.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/metis_tools.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/misc.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/mutual.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/nat_simprocs.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/nbe.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/normalizer.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/normalizer_data.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/numeral.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/numeral_syntax.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/order.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/outline.pdf -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/pattern_split.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/polyhash.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/post.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/presburger.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/primrec_package.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/project_rule.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/prop_logic.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/qelim.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/quantifier1.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/rat.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/recdef_package.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/recfun_codegen.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/record_package.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/refute.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/refute_isar.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/res_atp.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/res_atp_methods.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/res_atp_provers.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/res_axioms.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/res_clause.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/res_hol_clause.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/res_reconstruct.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/rewrite_hol_proof.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/rules.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/rw_inst.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/rw_tools.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/sat_funcs.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/sat_solver.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/session.graph -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/simpdata.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/size.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/small.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/specification_package.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/split_rule.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/splitter.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/string_syntax.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/tfl.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/thms.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/thry.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/trancl.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/typecopy_package.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/typedef_codegen.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/typedef_package.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/usyntax.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/utils.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/watcher.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/zipper.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/.session/entries %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/.session/pre-index %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Adm.html @@ -1678,7 +1480,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/IOA/Modelcheck/isabelle.css %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/IOA/Modelcheck/large.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/IOA/Modelcheck/medium.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/IOA/Modelcheck/mucke_oracle.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/IOA/Modelcheck/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/IOA/Modelcheck/small.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/IOA/NTP/.session/entries @@ -1737,7 +1538,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/IOA/ex/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/IOA/ex/small.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/IOA/index.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/IOA/ioa_package.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/IOA/isabelle.css %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/IOA/large.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/IOA/medium.html @@ -1753,15 +1553,7 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Ssum.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Tr.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Up.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/adm_tac.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/cont_consts.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/cont_proc.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/document.pdf -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/domain_axioms.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/domain_extender.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/domain_library.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/domain_syntax.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/domain_theorems.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/ex/.session/entries %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/ex/.session/pre-index %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/ex/Dagstuhl.html @@ -1780,16 +1572,20 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/ex/medium.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/ex/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/ex/small.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/fixrec_package.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/holcf_logic.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/index.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/isabelle.css %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/large.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/medium.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/outline.pdf -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/pcpodef_package.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/small.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Bifinite.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/CompactBasis.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/ConvexPD.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Countable.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/LowerPD.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/SetPcpo.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/UpperPD.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/LCF/.session/entries %%PORTDOCS%%%%DOCSDIR%%/browser_info/LCF/.session/pre-index %%PORTDOCS%%%%DOCSDIR%%/browser_info/LCF/GraphBrowser.jar @@ -1855,10 +1651,7 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/Sequents/isabelle.css %%PORTDOCS%%%%DOCSDIR%%/browser_info/Sequents/large.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/Sequents/medium.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/Sequents/modal.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/Sequents/prover.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/Sequents/session.graph -%%PORTDOCS%%%%DOCSDIR%%/browser_info/Sequents/simpdata.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/Sequents/small.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/.session/entries %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/.session/pre-index @@ -1944,7 +1737,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Constructible/outline.pdf %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Constructible/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Constructible/small.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Datatype.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Epsilon.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/EquivClass.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Finite.html @@ -1991,15 +1783,10 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Induct/outline.pdf %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Induct/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Induct/small.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Inductive.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/InfDatatype.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Int.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/IntArith.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/IntDiv.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/List.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Main.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Main_ZFC.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Nat.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/OrdQuant.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Order.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/OrderArith.html @@ -2062,11 +1849,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/WF.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/ZF.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Zorn.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/arith_data.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/cancel_numerals.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/cartprod.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/combine_numerals.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/datatype_package.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/document.pdf %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/equalities.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/ex/.session/entries @@ -2091,24 +1873,22 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/ex/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/ex/small.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/func.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/ind_cases.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/ind_syntax.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/index.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/induct_tacs.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/inductive_package.ML.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/int_arith.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/isabelle.css %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/large.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/medium.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/numeral_syntax.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/outline.pdf %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/pair.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/primrec_package.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/session.graph -%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/simpdata.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/small.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/typechk.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/upair.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Datatype_ZF.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Inductive_ZF.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Int_ZF.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/IntDiv_ZF.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/List_ZF.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Main_ZF.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Nat_ZF.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/index.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/isabelle.gif %%PORTDOCS%%%%DOCSDIR%%/browser_screenshot.eps @@ -2116,7 +1896,6 @@ bin/isatool %%PORTDOCS%%%%DOCSDIR%%/classes.pdf %%PORTDOCS%%%%DOCSDIR%%/codegen.dvi %%PORTDOCS%%%%DOCSDIR%%/codegen.pdf -%%PORTDOCS%%%%DOCSDIR%%/codegen_process.pdf %%PORTDOCS%%%%DOCSDIR%%/codegen_process.ps %%PORTDOCS%%%%DOCSDIR%%/functions.dvi %%PORTDOCS%%%%DOCSDIR%%/functions.pdf @@ -2172,7 +1951,15 @@ bin/isatool %%DATADIR%%/heaps/%%HEAPSUBDIR%%/FOL %%DATADIR%%/heaps/%%HEAPSUBDIR%%/FOLP %%DATADIR%%/heaps/%%HEAPSUBDIR%%/HOL +%%HEAP_HOL_ALGEBRA%%%%DATADIR%%/heaps/%%HEAPSUBDIR%%/HOL-Algebra +%%HEAP_HOL_COMPLEX%%%%DATADIR%%/heaps/%%HEAPSUBDIR%%/HOL-Complex +%%HEAP_HOL_COMPLEX_MATRIX%%%%DATADIR%%/heaps/%%HEAPSUBDIR%%/HOL-Complex-Matrix +%%HEAP_HOL_NOMINAL%%%%DATADIR%%/heaps/%%HEAPSUBDIR%%/HOL-Nominal +%%HEAP_HOL_WORD%%%%DATADIR%%/heaps/%%HEAPSUBDIR%%/HOL-Word +%%HEAP_HOL_TLA%%%%DATADIR%%/heaps/%%HEAPSUBDIR%%/TLA +%%HEAP_HOL_HOL4%%%%DATADIR%%/heaps/%%HEAPSUBDIR%%/HOL4 %%DATADIR%%/heaps/%%HEAPSUBDIR%%/HOLCF +%%HEAP_HOLCF_IOA%%%%DATADIR%%/heaps/%%HEAPSUBDIR%%/IOA %%DATADIR%%/heaps/%%HEAPSUBDIR%%/LCF %%DATADIR%%/heaps/%%HEAPSUBDIR%%/Pure %%DATADIR%%/heaps/%%HEAPSUBDIR%%/Sequents @@ -2182,12 +1969,37 @@ bin/isatool %%DATADIR%%/heaps/%%HEAPSUBDIR%%/log/FOL.gz %%DATADIR%%/heaps/%%HEAPSUBDIR%%/log/FOLP.gz %%DATADIR%%/heaps/%%HEAPSUBDIR%%/log/HOL.gz +%%HEAP_HOL_ALGEBRA%%%%DATADIR%%/heaps/%%HEAPSUBDIR%%/log/HOL-Algebra.gz +%%HEAP_HOL_COMPLEX%%%%DATADIR%%/heaps/%%HEAPSUBDIR%%/log/HOL-Complex.gz +%%HEAP_HOL_COMPLEX_MATRIX%%%%DATADIR%%/heaps/%%HEAPSUBDIR%%/log/HOL-Complex-Matrix.gz +%%HEAP_HOL_NOMINAL%%%%DATADIR%%/heaps/%%HEAPSUBDIR%%/log/HOL-Nominal.gz +%%HEAP_HOL_WORD%%%%DATADIR%%/heaps/%%HEAPSUBDIR%%/log/HOL-Word.gz +%%HEAP_HOL_TLA%%%%DATADIR%%/heaps/%%HEAPSUBDIR%%/log/TLA.gz +%%HEAP_HOL_HOL4%%%%DATADIR%%/heaps/%%HEAPSUBDIR%%/log/HOL4.gz %%DATADIR%%/heaps/%%HEAPSUBDIR%%/log/HOLCF.gz +%%HEAP_HOLCF_IOA%%%%DATADIR%%/heaps/%%HEAPSUBDIR%%/log/IOA.gz %%DATADIR%%/heaps/%%HEAPSUBDIR%%/log/LCF.gz %%DATADIR%%/heaps/%%HEAPSUBDIR%%/log/Pure-Cube.gz %%DATADIR%%/heaps/%%HEAPSUBDIR%%/log/Pure.gz %%DATADIR%%/heaps/%%HEAPSUBDIR%%/log/Sequents.gz %%DATADIR%%/heaps/%%HEAPSUBDIR%%/log/ZF.gz +%%DATADIR%%/lib/classes/isabelle/IsabelleDemo.java +%%DATADIR%%/lib/classes/isabelle/IsabelleProcess.java +%%DATADIR%%/lib/classes/isabelle.jar +%%DATADIR%%/lib/classes/mk +%%DATADIR%%/lib/jedit/plugin/isabelle/IsabelleDock.scala +%%DATADIR%%/lib/jedit/plugin/isabelle/IsabelleParser.scala +%%DATADIR%%/lib/jedit/plugin/isabelle/IsabellePlugin.scala +%%DATADIR%%/lib/jedit/plugin/Isabelle.props +%%DATADIR%%/lib/jedit/plugin/dockables.xml +%%DATADIR%%/lib/jedit/plugin/services.xml +%%DATADIR%%/lib/jedit/plugin/mk +%%DATADIR%%/lib/jedit/isabelle.jar +%%DATADIR%%/lib/scripts/system.pl +%%DATADIR%%/lib/scripts/yxml.pl +%%DATADIR%%/lib/scripts/run-polyml-4.1.3 +%%DATADIR%%/lib/scripts/run-polyml-4.1.4 +%%DATADIR%%/lib/scripts/run-polyml-4.2.0 %%DATADIR%%/lib/ProofGeneral/README %%DATADIR%%/lib/ProofGeneral/pgip.rnc %%DATADIR%%/lib/ProofGeneral/pgip_isar.xml @@ -2200,12 +2012,8 @@ bin/isatool %%DATADIR%%/lib/Tools/display %%DATADIR%%/lib/Tools/doc %%DATADIR%%/lib/Tools/document -%%DATADIR%%/lib/Tools/expandshort %%DATADIR%%/lib/Tools/findlogics -%%DATADIR%%/lib/Tools/fixcpure -%%DATADIR%%/lib/Tools/fixgreek %%DATADIR%%/lib/Tools/fixheaders -%%DATADIR%%/lib/Tools/fixsome %%DATADIR%%/lib/Tools/getenv %%DATADIR%%/lib/Tools/install %%DATADIR%%/lib/Tools/keywords @@ -2216,6 +2024,8 @@ bin/isatool %%DATADIR%%/lib/Tools/mkdir %%DATADIR%%/lib/Tools/mkproject %%DATADIR%%/lib/Tools/print +%%DATADIR%%/lib/Tools/tty +%%DATADIR%%/lib/Tools/yxml %%DATADIR%%/lib/Tools/unsymbolize %%DATADIR%%/lib/Tools/usedir %%DATADIR%%/lib/Tools/version @@ -2263,26 +2073,19 @@ bin/isatool %%DATADIR%%/lib/logo/isabelle_transparent.gif %%DATADIR%%/lib/logo/isabelle_zf.eps %%DATADIR%%/lib/logo/isabelle_zf.gif -%%DATADIR%%/lib/scripts/configure %%DATADIR%%/lib/scripts/convert.pl %%DATADIR%%/lib/scripts/dimacs2hol.pl -%%DATADIR%%/lib/scripts/expandshort.pl %%DATADIR%%/lib/scripts/feeder %%DATADIR%%/lib/scripts/feeder.pl %%DATADIR%%/lib/scripts/fileident -%%DATADIR%%/lib/scripts/fixcpure.pl -%%DATADIR%%/lib/scripts/fixgreek.pl %%DATADIR%%/lib/scripts/fixheaders.pl -%%DATADIR%%/lib/scripts/fixsome.pl %%DATADIR%%/lib/scripts/getsettings %%DATADIR%%/lib/scripts/keywords.pl -%%DATADIR%%/lib/scripts/patch-scripts.bash %%DATADIR%%/lib/scripts/polyml-platform %%DATADIR%%/lib/scripts/polyml-version %%DATADIR%%/lib/scripts/run-mosml %%DATADIR%%/lib/scripts/run-polyml %%DATADIR%%/lib/scripts/run-polyml-5.0 -%%DATADIR%%/lib/scripts/run-polyml-5.1 %%DATADIR%%/lib/scripts/run-poplogml %%DATADIR%%/lib/scripts/run-smlnj %%DATADIR%%/lib/scripts/timestart.bash @@ -2359,31 +2162,28 @@ bin/isatool %%DATADIR%%/src/FOL/intprover.ML %%DATADIR%%/src/FOL/simpdata.ML %%DATADIR%%/src/FOLP/FOLP.thy -%%DATADIR%%/src/FOLP/FOLP_lemmas.ML -%%DATADIR%%/src/FOLP/IFOLP.ML %%DATADIR%%/src/FOLP/IFOLP.thy %%DATADIR%%/src/FOLP/IsaMakefile %%DATADIR%%/src/FOLP/ROOT.ML %%DATADIR%%/src/FOLP/classical.ML -%%DATADIR%%/src/FOLP/ex/If.ML %%DATADIR%%/src/FOLP/ex/If.thy -%%DATADIR%%/src/FOLP/ex/Nat.ML %%DATADIR%%/src/FOLP/ex/Nat.thy %%DATADIR%%/src/FOLP/ex/Prolog.ML %%DATADIR%%/src/FOLP/ex/Prolog.thy %%DATADIR%%/src/FOLP/ex/ROOT.ML -%%DATADIR%%/src/FOLP/ex/cla.ML -%%DATADIR%%/src/FOLP/ex/foundn.ML -%%DATADIR%%/src/FOLP/ex/int.ML -%%DATADIR%%/src/FOLP/ex/intro.ML -%%DATADIR%%/src/FOLP/ex/prop.ML -%%DATADIR%%/src/FOLP/ex/quant.ML +%%DATADIR%%/src/FOLP/ex/Classical.thy +%%DATADIR%%/src/FOLP/ex/Foundation.thy +%%DATADIR%%/src/FOLP/ex/Intro.thy +%%DATADIR%%/src/FOLP/ex/Intuitionistic.thy +%%DATADIR%%/src/FOLP/ex/Propositional_Cla.thy +%%DATADIR%%/src/FOLP/ex/Propositional_Int.thy +%%DATADIR%%/src/FOLP/ex/Quantifiers_Cla.thy +%%DATADIR%%/src/FOLP/ex/Quantifiers_Int.thy %%DATADIR%%/src/FOLP/hypsubst.ML %%DATADIR%%/src/FOLP/intprover.ML %%DATADIR%%/src/FOLP/simp.ML %%DATADIR%%/src/FOLP/simpdata.ML %%DATADIR%%/src/HOL/ATP_Linkup.thy -%%DATADIR%%/src/HOL/Accessible_Part.thy %%DATADIR%%/src/HOL/Algebra/AbelCoset.thy %%DATADIR%%/src/HOL/Algebra/Bij.thy %%DATADIR%%/src/HOL/Algebra/Coset.thy @@ -2416,6 +2216,36 @@ bin/isatool %%DATADIR%%/src/HOL/Algebra/poly/UnivPoly2.thy %%DATADIR%%/src/HOL/Algebra/ringsimp.ML %%DATADIR%%/src/HOL/Arith_Tools.thy +%%DATADIR%%/src/HOL/Complex/Fundamental_Theorem_Algebra.thy +%%DATADIR%%/src/HOL/Library/Array.thy +%%DATADIR%%/src/HOL/Library/Countable.thy +%%DATADIR%%/src/HOL/Library/Dense_Linear_Order.thy +%%DATADIR%%/src/HOL/Library/Enum.thy +%%DATADIR%%/src/HOL/Library/Heap.thy +%%DATADIR%%/src/HOL/Library/Heap_Monad.thy +%%DATADIR%%/src/HOL/Library/Imperative_HOL.thy +%%DATADIR%%/src/HOL/Library/ListVector.thy +%%DATADIR%%/src/HOL/Library/Option_ord.thy +%%DATADIR%%/src/HOL/Library/Order_Relation.thy +%%DATADIR%%/src/HOL/Library/Pocklington.thy +%%DATADIR%%/src/HOL/Library/RBT.thy +%%DATADIR%%/src/HOL/Library/RType.thy +%%DATADIR%%/src/HOL/Library/Ref.thy +%%DATADIR%%/src/HOL/Library/Sublist_Order.thy +%%DATADIR%%/src/HOL/Library/Univ_Poly.thy +%%DATADIR%%/src/HOL/Nominal/Examples/Contexts.thy +%%DATADIR%%/src/HOL/Nominal/Examples/Type_Preservation.thy +%%DATADIR%%/src/HOL/Nominal/Examples/VC_Condition.thy +%%DATADIR%%/src/HOL/Nominal/Examples/W.thy +%%DATADIR%%/src/HOL/Tools/function_package/induction_scheme.ML +%%DATADIR%%/src/HOL/Tools/function_package/measure_functions.ML +%%DATADIR%%/src/HOL/Tools/function_package/sum_tree.ML +%%DATADIR%%/src/HOL/Tools/old_primrec_package.ML +%%DATADIR%%/src/HOL/ex/Efficient_Nat_examples.thy +%%DATADIR%%/src/HOL/ex/Induction_Scheme.thy +%%DATADIR%%/src/HOL/ex/Quickcheck.thy +%%DATADIR%%/src/HOL/Int.thy +%%DATADIR%%/src/HOL/Wellfounded.thy %%DATADIR%%/src/HOL/Auth/CertifiedEmail.thy %%DATADIR%%/src/HOL/Auth/Event.thy %%DATADIR%%/src/HOL/Auth/Guard/Analz.thy @@ -2578,7 +2408,6 @@ bin/isatool %%DATADIR%%/src/HOL/HoareParallel/document/root.bib %%DATADIR%%/src/HOL/HoareParallel/document/root.tex %%DATADIR%%/src/HOL/Hyperreal/Deriv.thy -%%DATADIR%%/src/HOL/Hyperreal/EvenOdd.thy %%DATADIR%%/src/HOL/Hyperreal/Fact.thy %%DATADIR%%/src/HOL/Hyperreal/Filter.thy %%DATADIR%%/src/HOL/Hyperreal/FrechetDeriv.thy @@ -2603,7 +2432,6 @@ bin/isatool %%DATADIR%%/src/HOL/Hyperreal/SEQ.thy %%DATADIR%%/src/HOL/Hyperreal/Series.thy %%DATADIR%%/src/HOL/Hyperreal/Star.thy -%%DATADIR%%/src/HOL/Hyperreal/StarClasses.thy %%DATADIR%%/src/HOL/Hyperreal/StarDef.thy %%DATADIR%%/src/HOL/Hyperreal/Taylor.thy %%DATADIR%%/src/HOL/Hyperreal/Transcendental.thy @@ -2743,8 +2571,6 @@ bin/isatool %%DATADIR%%/src/HOL/Induct/Tree.thy %%DATADIR%%/src/HOL/Induct/document/root.tex %%DATADIR%%/src/HOL/Inductive.thy -%%DATADIR%%/src/HOL/IntArith.thy -%%DATADIR%%/src/HOL/IntDef.thy %%DATADIR%%/src/HOL/IntDiv.thy %%DATADIR%%/src/HOL/IsaMakefile %%DATADIR%%/src/HOL/Isar_examples/BasicLogic.thy @@ -2831,7 +2657,6 @@ bin/isatool %%DATADIR%%/src/HOL/Library/Permutation.thy %%DATADIR%%/src/HOL/Library/Primes.thy %%DATADIR%%/src/HOL/Library/Product_ord.thy -%%DATADIR%%/src/HOL/Library/Pure_term.thy %%DATADIR%%/src/HOL/Library/Quicksort.thy %%DATADIR%%/src/HOL/Library/Quotient.thy %%DATADIR%%/src/HOL/Library/README.html @@ -2966,7 +2791,6 @@ bin/isatool %%DATADIR%%/src/HOL/Nominal/Examples/SN.thy %%DATADIR%%/src/HOL/Nominal/Examples/SOS.thy %%DATADIR%%/src/HOL/Nominal/Examples/Support.thy -%%DATADIR%%/src/HOL/Nominal/Examples/VC_Compatible.thy %%DATADIR%%/src/HOL/Nominal/Examples/Weakening.thy %%DATADIR%%/src/HOL/Nominal/INSTALL %%DATADIR%%/src/HOL/Nominal/Nominal.thy @@ -2997,11 +2821,9 @@ bin/isatool %%DATADIR%%/src/HOL/NumberTheory/WilsonBij.thy %%DATADIR%%/src/HOL/NumberTheory/WilsonRuss.thy %%DATADIR%%/src/HOL/NumberTheory/document/root.tex -%%DATADIR%%/src/HOL/Numeral.thy %%DATADIR%%/src/HOL/OrderedGroup.thy %%DATADIR%%/src/HOL/Orderings.thy %%DATADIR%%/src/HOL/Power.thy -%%DATADIR%%/src/HOL/PreList.thy %%DATADIR%%/src/HOL/Predicate.thy %%DATADIR%%/src/HOL/Presburger.thy %%DATADIR%%/src/HOL/Product_Type.thy @@ -3097,7 +2919,6 @@ bin/isatool %%DATADIR%%/src/HOL/TLA/Inc/ROOT.ML %%DATADIR%%/src/HOL/TLA/Init.thy %%DATADIR%%/src/HOL/TLA/Intensional.thy -%%DATADIR%%/src/HOL/TLA/Memory/MIParameters.thy %%DATADIR%%/src/HOL/TLA/Memory/MemClerk.thy %%DATADIR%%/src/HOL/TLA/Memory/MemClerkParameters.thy %%DATADIR%%/src/HOL/TLA/Memory/Memory.thy @@ -3249,8 +3070,6 @@ bin/isatool %%DATADIR%%/src/HOL/W0/ROOT.ML %%DATADIR%%/src/HOL/W0/W0.thy %%DATADIR%%/src/HOL/W0/document/root.tex -%%DATADIR%%/src/HOL/Wellfounded_Recursion.thy -%%DATADIR%%/src/HOL/Wellfounded_Relations.thy %%DATADIR%%/src/HOL/Word/BinBoolList.thy %%DATADIR%%/src/HOL/Word/BinGeneral.thy %%DATADIR%%/src/HOL/Word/BinOperations.thy @@ -3290,7 +3109,6 @@ bin/isatool %%DATADIR%%/src/HOL/ex/CTL.thy %%DATADIR%%/src/HOL/ex/Chinese.thy %%DATADIR%%/src/HOL/ex/Classical.thy -%%DATADIR%%/src/HOL/ex/Classpackage.thy %%DATADIR%%/src/HOL/ex/Codegenerator.thy %%DATADIR%%/src/HOL/ex/Codegenerator_Pretty.thy %%DATADIR%%/src/HOL/ex/Commutative_RingEx.thy @@ -3317,7 +3135,6 @@ bin/isatool %%DATADIR%%/src/HOL/ex/Meson_Test.thy %%DATADIR%%/src/HOL/ex/MonoidGroup.thy %%DATADIR%%/src/HOL/ex/Multiquote.thy -%%DATADIR%%/src/HOL/ex/NBE.thy %%DATADIR%%/src/HOL/ex/NatSum.thy %%DATADIR%%/src/HOL/ex/NormalForm.thy %%DATADIR%%/src/HOL/ex/PER.thy @@ -3373,6 +3190,12 @@ bin/isatool %%DATADIR%%/src/HOLCF/Fix.thy %%DATADIR%%/src/HOLCF/Fixrec.thy %%DATADIR%%/src/HOLCF/HOLCF.thy +%%DATADIR%%/src/HOLCF/Bifinite.thy +%%DATADIR%%/src/HOLCF/CompactBasis.thy +%%DATADIR%%/src/HOLCF/ConvexPD.thy +%%DATADIR%%/src/HOLCF/LowerPD.thy +%%DATADIR%%/src/HOLCF/SetPcpo.thy +%%DATADIR%%/src/HOLCF/UpperPD.thy %%DATADIR%%/src/HOLCF/IMP/Denotational.thy %%DATADIR%%/src/HOLCF/IMP/HoareEx.thy %%DATADIR%%/src/HOLCF/IMP/README.html @@ -3509,7 +3332,6 @@ bin/isatool %%DATADIR%%/src/Provers/splitter.ML %%DATADIR%%/src/Provers/trancl.ML %%DATADIR%%/src/Provers/typedsimp.ML -%%DATADIR%%/src/Pure/CPure.thy %%DATADIR%%/src/Pure/General/ROOT.ML %%DATADIR%%/src/Pure/General/alist.ML %%DATADIR%%/src/Pure/General/balanced_tree.ML @@ -3590,8 +3412,6 @@ bin/isatool %%DATADIR%%/src/Pure/ML-Systems/polyml-4.1.4.ML %%DATADIR%%/src/Pure/ML-Systems/polyml-5.0.ML %%DATADIR%%/src/Pure/ML-Systems/polyml-5.1.ML -%%DATADIR%%/src/Pure/ML-Systems/polyml-old-basis.ML -%%DATADIR%%/src/Pure/ML-Systems/polyml-posix.ML %%DATADIR%%/src/Pure/ML-Systems/polyml.ML %%DATADIR%%/src/Pure/ML-Systems/poplogml.ML %%DATADIR%%/src/Pure/ML-Systems/proper_int.ML @@ -3640,7 +3460,6 @@ bin/isatool %%DATADIR%%/src/Pure/Thy/latex.ML %%DATADIR%%/src/Pure/Thy/present.ML %%DATADIR%%/src/Pure/Thy/term_style.ML -%%DATADIR%%/src/Pure/Thy/thm_database.ML %%DATADIR%%/src/Pure/Thy/thm_deps.ML %%DATADIR%%/src/Pure/Thy/thy_edit.ML %%DATADIR%%/src/Pure/Thy/thy_header.ML @@ -3655,18 +3474,15 @@ bin/isatool %%DATADIR%%/src/Pure/assumption.ML %%DATADIR%%/src/Pure/axclass.ML %%DATADIR%%/src/Pure/codegen.ML -%%DATADIR%%/src/Pure/compress.ML %%DATADIR%%/src/Pure/config.ML %%DATADIR%%/src/Pure/conjunction.ML %%DATADIR%%/src/Pure/consts.ML %%DATADIR%%/src/Pure/context.ML -%%DATADIR%%/src/Pure/context_position.ML %%DATADIR%%/src/Pure/conv.ML %%DATADIR%%/src/Pure/defs.ML %%DATADIR%%/src/Pure/display.ML %%DATADIR%%/src/Pure/drule.ML %%DATADIR%%/src/Pure/envir.ML -%%DATADIR%%/src/Pure/fact_index.ML %%DATADIR%%/src/Pure/goal.ML %%DATADIR%%/src/Pure/interpretation.ML %%DATADIR%%/src/Pure/library.ML @@ -3698,6 +3514,18 @@ bin/isatool %%DATADIR%%/src/Pure/type_infer.ML %%DATADIR%%/src/Pure/unify.ML %%DATADIR%%/src/Pure/variable.ML +%%DATADIR%%/src/Pure/General/yxml.ML +%%DATADIR%%/src/Pure/Isar/isar.ML +%%DATADIR%%/src/Pure/Isar/overloading.ML +%%DATADIR%%/src/Pure/ML-Systems/polyml-4.2.0.ML +%%DATADIR%%/src/Pure/ML-Systems/polyml_common.ML +%%DATADIR%%/src/Pure/ML-Systems/polyml_old_basis.ML +%%DATADIR%%/src/Pure/ML-Systems/polyml_old_compiler4.ML +%%DATADIR%%/src/Pure/ML-Systems/polyml_old_compiler5.ML +%%DATADIR%%/src/Pure/ML-Systems/system_shell.ML +%%DATADIR%%/src/Pure/ML-Systems/universal.ML +%%DATADIR%%/src/Pure/Tools/isabelle_process.ML +%%DATADIR%%/src/Pure/facts.ML %%DATADIR%%/src/Sequents/ILL.thy %%DATADIR%%/src/Sequents/ILL_predlog.thy %%DATADIR%%/src/Sequents/IsaMakefile @@ -3783,13 +3611,10 @@ bin/isatool %%DATADIR%%/src/Tools/Metis/src/PortableIsabelle.sml %%DATADIR%%/src/Tools/Metis/src/PortableMlton.sml %%DATADIR%%/src/Tools/Metis/src/PortableMosml.sml -%%DATADIR%%/src/Tools/Metis/src/PortableSmlNJ.sml %%DATADIR%%/src/Tools/Metis/src/Problem.sig %%DATADIR%%/src/Tools/Metis/src/Problem.sml %%DATADIR%%/src/Tools/Metis/src/Proof.sig %%DATADIR%%/src/Tools/Metis/src/Proof.sml -%%DATADIR%%/src/Tools/Metis/src/Random.sig -%%DATADIR%%/src/Tools/Metis/src/Random.sml %%DATADIR%%/src/Tools/Metis/src/RandomMap.sml %%DATADIR%%/src/Tools/Metis/src/RandomSet.sml %%DATADIR%%/src/Tools/Metis/src/Resolution.sig @@ -3836,6 +3661,8 @@ bin/isatool %%DATADIR%%/src/Tools/induct.ML %%DATADIR%%/src/Tools/nbe.ML %%DATADIR%%/src/Tools/rat.ML +%%DATADIR%%/src/Tools/atomize_elim.ML +%%DATADIR%%/src/Tools/random_word.ML %%DATADIR%%/src/ZF/AC.thy %%DATADIR%%/src/ZF/AC/AC15_WO6.thy %%DATADIR%%/src/ZF/AC/AC16_WO4.thy @@ -3894,7 +3721,6 @@ bin/isatool %%DATADIR%%/src/ZF/Constructible/Wellorderings.thy %%DATADIR%%/src/ZF/Constructible/document/root.bib %%DATADIR%%/src/ZF/Constructible/document/root.tex -%%DATADIR%%/src/ZF/Datatype.thy %%DATADIR%%/src/ZF/Epsilon.thy %%DATADIR%%/src/ZF/EquivClass.thy %%DATADIR%%/src/ZF/Finite.thy @@ -3923,16 +3749,11 @@ bin/isatool %%DATADIR%%/src/ZF/Induct/Term.thy %%DATADIR%%/src/ZF/Induct/Tree_Forest.thy %%DATADIR%%/src/ZF/Induct/document/root.tex -%%DATADIR%%/src/ZF/Inductive.thy %%DATADIR%%/src/ZF/InfDatatype.thy -%%DATADIR%%/src/ZF/Int.thy %%DATADIR%%/src/ZF/IntArith.thy -%%DATADIR%%/src/ZF/IntDiv.thy %%DATADIR%%/src/ZF/IsaMakefile -%%DATADIR%%/src/ZF/List.thy %%DATADIR%%/src/ZF/Main.thy %%DATADIR%%/src/ZF/Main_ZFC.thy -%%DATADIR%%/src/ZF/Nat.thy %%DATADIR%%/src/ZF/OrdQuant.thy %%DATADIR%%/src/ZF/Order.thy %%DATADIR%%/src/ZF/OrderArith.thy @@ -4008,6 +3829,13 @@ bin/isatool %%DATADIR%%/src/ZF/pair.thy %%DATADIR%%/src/ZF/simpdata.ML %%DATADIR%%/src/ZF/upair.thy +%%DATADIR%%/src/ZF/Datatype_ZF.thy +%%DATADIR%%/src/ZF/Inductive_ZF.thy +%%DATADIR%%/src/ZF/Int_ZF.thy +%%DATADIR%%/src/ZF/IntDiv_ZF.thy +%%DATADIR%%/src/ZF/List_ZF.thy +%%DATADIR%%/src/ZF/Main_ZF.thy +%%DATADIR%%/src/ZF/Nat_ZF.thy @dirrm %%DATADIR%%/src/ZF/ex @dirrm %%DATADIR%%/src/ZF/document @dirrm %%DATADIR%%/src/ZF/UNITY @@ -4173,12 +4001,16 @@ bin/isatool @dirrm %%DATADIR%%/lib/texinputs @dirrm %%DATADIR%%/lib/scripts @dirrm %%DATADIR%%/lib/logo +@dirrm %%DATADIR%%/lib/jedit/plugin/isabelle +@dirrm %%DATADIR%%/lib/jedit/plugin @dirrm %%DATADIR%%/lib/jedit @dirrm %%DATADIR%%/lib/icons @dirrm %%DATADIR%%/lib/html @dirrm %%DATADIR%%/lib/browser/awtUtilities @dirrm %%DATADIR%%/lib/browser/GraphBrowser @dirrm %%DATADIR%%/lib/browser +@dirrm %%DATADIR%%/lib/classes/isabelle +@dirrm %%DATADIR%%/lib/classes @dirrm %%DATADIR%%/lib/Tools @dirrm %%DATADIR%%/lib/ProofGeneral @dirrm %%DATADIR%%/lib |