Attachment 89189 Details for Bug 126067 – isabelle-2008.patch

[patch] isabelle-2008.patch

isabelle-2008.patch (text/plain), 117.20 KB, created by Timothy Bourke on 2008-07-29 07:50:02 UTC

(hide)

Description:

Filename:

MIME Type:

Creator: Timothy Bourke

Created: 2008-07-29 07:50:02 UTC

Size: 117.20 KB

patch

obsolete

>Index: Makefile
>===================================================================
>RCS file: /home/ncvs/ports/math/isabelle/Makefile,v
>retrieving revision 1.9
>diff -u -r1.9 Makefile
>--- Makefile	6 Jun 2008 13:43:59 -0000	1.9
>+++ Makefile	29 Jul 2008 06:32:26 -0000
>@@ -2,54 +2,126 @@
> # Date created:        08 August 2005
> # Whom:                Timothy Bourke <timbob@bigpond.com>
> #
>-# $FreeBSD: ports/math/isabelle/Makefile,v 1.9 2008/06/06 13:43:59 edwin Exp $
>+# $FreeBSD$
> #
> 
> 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 @@
> 		 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)
>Index: distinfo
>===================================================================
>RCS file: /home/ncvs/ports/math/isabelle/distinfo,v
>retrieving revision 1.4
>diff -u -r1.4 distinfo
>--- distinfo	4 Apr 2008 12:15:21 -0000	1.4
>+++ distinfo	29 Jul 2008 06:32:26 -0000
>@@ -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
>Index: pkg-plist
>===================================================================
>RCS file: /home/ncvs/ports/math/isabelle/pkg-plist,v
>retrieving revision 1.6
>diff -u -r1.6 pkg-plist
>--- pkg-plist	4 Apr 2008 12:15:21 -0000	1.6
>+++ pkg-plist	29 Jul 2008 06:32:28 -0000
>@@ -4,8 +4,6 @@
> 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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> %%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 @@
> @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
>Index: files/patch-bin-Isabelle
>===================================================================
>RCS file: files/patch-bin-Isabelle
>diff -N files/patch-bin-Isabelle
>--- files/patch-bin-Isabelle	10 Sep 2007 12:11:09 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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
>Index: files/patch-bin-isabelle
>===================================================================
>RCS file: files/patch-bin-isabelle
>diff -N files/patch-bin-isabelle
>--- files/patch-bin-isabelle	10 Sep 2007 12:11:09 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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
>Index: files/patch-bin-isabelle_interface
>===================================================================
>RCS file: files/patch-bin-isabelle_interface
>diff -N files/patch-bin-isabelle_interface
>--- files/patch-bin-isabelle_interface	10 Sep 2007 12:11:09 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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
>Index: files/patch-bin-isabelle_process
>===================================================================
>RCS file: files/patch-bin-isabelle_process
>diff -N files/patch-bin-isabelle_process
>--- files/patch-bin-isabelle_process	4 Apr 2008 12:15:22 -0000	1.2
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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
>Index: files/patch-bin-isatool
>===================================================================
>RCS file: files/patch-bin-isatool
>diff -N files/patch-bin-isatool
>--- files/patch-bin-isatool	10 Sep 2007 12:11:09 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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
>Index: files/patch-build
>===================================================================
>RCS file: files/patch-build
>diff -N files/patch-build
>--- files/patch-build	4 Apr 2008 12:15:22 -0000	1.2
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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
>Index: files/patch-etc-settings
>===================================================================
>RCS file: /home/ncvs/ports/math/isabelle/files/patch-etc-settings,v
>retrieving revision 1.4
>diff -u -r1.4 patch-etc-settings
>--- files/patch-etc-settings	4 Apr 2008 12:15:22 -0000	1.4
>+++ files/patch-etc-settings	29 Jul 2008 06:32:28 -0000
>@@ -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" "")
>Index: files/patch-lib-Tools-browser
>===================================================================
>RCS file: files/patch-lib-Tools-browser
>diff -N files/patch-lib-Tools-browser
>--- files/patch-lib-Tools-browser	4 Apr 2008 12:15:22 -0000	1.2
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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
>Index: files/patch-lib-Tools-codegen
>===================================================================
>RCS file: files/patch-lib-Tools-codegen
>diff -N files/patch-lib-Tools-codegen
>--- files/patch-lib-Tools-codegen	4 Apr 2008 12:15:22 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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"
>Index: files/patch-lib-Tools-convert
>===================================================================
>RCS file: files/patch-lib-Tools-convert
>diff -N files/patch-lib-Tools-convert
>--- files/patch-lib-Tools-convert	10 Sep 2007 12:11:09 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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...]"
>Index: files/patch-lib-Tools-dimacs2hol
>===================================================================
>RCS file: files/patch-lib-Tools-dimacs2hol
>diff -N files/patch-lib-Tools-dimacs2hol
>--- files/patch-lib-Tools-dimacs2hol	10 Sep 2007 12:11:09 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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"
>Index: files/patch-lib-Tools-display
>===================================================================
>RCS file: files/patch-lib-Tools-display
>diff -N files/patch-lib-Tools-display
>--- files/patch-lib-Tools-display	4 Apr 2008 12:15:22 -0000	1.2
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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
>Index: files/patch-lib-Tools-doc
>===================================================================
>RCS file: files/patch-lib-Tools-doc
>diff -N files/patch-lib-Tools-doc
>--- files/patch-lib-Tools-doc	10 Sep 2007 12:11:09 -0000	1.3
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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
>Index: files/patch-lib-Tools-document
>===================================================================
>RCS file: files/patch-lib-Tools-document
>diff -N files/patch-lib-Tools-document
>--- files/patch-lib-Tools-document	10 Sep 2007 12:11:09 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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
>Index: files/patch-lib-Tools-expandshort
>===================================================================
>RCS file: files/patch-lib-Tools-expandshort
>diff -N files/patch-lib-Tools-expandshort
>--- files/patch-lib-Tools-expandshort	10 Sep 2007 12:11:09 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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...]"
>Index: files/patch-lib-Tools-findlogics
>===================================================================
>RCS file: files/patch-lib-Tools-findlogics
>diff -N files/patch-lib-Tools-findlogics
>--- files/patch-lib-Tools-findlogics	4 Apr 2008 12:15:22 -0000	1.2
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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"
>Index: files/patch-lib-Tools-fixcpure
>===================================================================
>RCS file: files/patch-lib-Tools-fixcpure
>diff -N files/patch-lib-Tools-fixcpure
>--- files/patch-lib-Tools-fixcpure	10 Sep 2007 12:11:09 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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...]"
>Index: files/patch-lib-Tools-fixgreek
>===================================================================
>RCS file: files/patch-lib-Tools-fixgreek
>diff -N files/patch-lib-Tools-fixgreek
>--- files/patch-lib-Tools-fixgreek	10 Sep 2007 12:11:09 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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...]"
>Index: files/patch-lib-Tools-fixheaders
>===================================================================
>RCS file: files/patch-lib-Tools-fixheaders
>diff -N files/patch-lib-Tools-fixheaders
>--- files/patch-lib-Tools-fixheaders	10 Sep 2007 12:11:09 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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...]"
>Index: files/patch-lib-Tools-fixsome
>===================================================================
>RCS file: files/patch-lib-Tools-fixsome
>diff -N files/patch-lib-Tools-fixsome
>--- files/patch-lib-Tools-fixsome	10 Sep 2007 12:11:09 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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...]"
>Index: files/patch-lib-Tools-getenv
>===================================================================
>RCS file: files/patch-lib-Tools-getenv
>diff -N files/patch-lib-Tools-getenv
>--- files/patch-lib-Tools-getenv	10 Sep 2007 12:11:09 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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 ...]"
>Index: files/patch-lib-Tools-install
>===================================================================
>RCS file: files/patch-lib-Tools-install
>diff -N files/patch-lib-Tools-install
>--- files/patch-lib-Tools-install	10 Sep 2007 12:11:09 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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"
>Index: files/patch-lib-Tools-keywords
>===================================================================
>RCS file: files/patch-lib-Tools-keywords
>diff -N files/patch-lib-Tools-keywords
>--- files/patch-lib-Tools-keywords	4 Apr 2008 12:15:22 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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 ...]"
>Index: files/patch-lib-Tools-latex
>===================================================================
>RCS file: files/patch-lib-Tools-latex
>diff -N files/patch-lib-Tools-latex
>--- files/patch-lib-Tools-latex	10 Sep 2007 12:11:09 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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";' \
>Index: files/patch-lib-Tools-logo
>===================================================================
>RCS file: files/patch-lib-Tools-logo
>diff -N files/patch-lib-Tools-logo
>--- files/patch-lib-Tools-logo	10 Sep 2007 12:11:09 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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
>Index: files/patch-lib-Tools-make
>===================================================================
>RCS file: files/patch-lib-Tools-make
>diff -N files/patch-lib-Tools-make
>--- files/patch-lib-Tools-make	10 Sep 2007 12:11:09 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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 ...]"
>Index: files/patch-lib-Tools-makeall
>===================================================================
>RCS file: files/patch-lib-Tools-makeall
>diff -N files/patch-lib-Tools-makeall
>--- files/patch-lib-Tools-makeall	4 Apr 2008 12:15:22 -0000	1.2
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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
>Index: files/patch-lib-Tools-mkdir
>===================================================================
>RCS file: files/patch-lib-Tools-mkdir
>diff -N files/patch-lib-Tools-mkdir
>--- files/patch-lib-Tools-mkdir	4 Apr 2008 12:15:22 -0000	1.2
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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
>Index: files/patch-lib-Tools-mkproject
>===================================================================
>RCS file: files/patch-lib-Tools-mkproject
>diff -N files/patch-lib-Tools-mkproject
>--- files/patch-lib-Tools-mkproject	4 Apr 2008 12:15:22 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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"
>Index: files/patch-lib-Tools-print
>===================================================================
>RCS file: files/patch-lib-Tools-print
>diff -N files/patch-lib-Tools-print
>--- files/patch-lib-Tools-print	10 Sep 2007 12:11:09 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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
>Index: files/patch-lib-Tools-unsymbolize
>===================================================================
>RCS file: files/patch-lib-Tools-unsymbolize
>diff -N files/patch-lib-Tools-unsymbolize
>--- files/patch-lib-Tools-unsymbolize	10 Sep 2007 12:11:09 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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...]"
>Index: files/patch-lib-Tools-usedir
>===================================================================
>RCS file: files/patch-lib-Tools-usedir
>diff -N files/patch-lib-Tools-usedir
>--- files/patch-lib-Tools-usedir	4 Apr 2008 12:15:22 -0000	1.2
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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
>Index: files/patch-lib-Tools-version
>===================================================================
>RCS file: files/patch-lib-Tools-version
>diff -N files/patch-lib-Tools-version
>--- files/patch-lib-Tools-version	4 Apr 2008 12:15:22 -0000	1.2
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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
>Index: files/patch-lib-scripts-configure
>===================================================================
>RCS file: files/patch-lib-scripts-configure
>diff -N files/patch-lib-scripts-configure
>--- files/patch-lib-scripts-configure	4 Apr 2008 12:15:22 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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
>Index: files/patch-lib-scripts-feeder
>===================================================================
>RCS file: files/patch-lib-scripts-feeder
>diff -N files/patch-lib-scripts-feeder
>--- files/patch-lib-scripts-feeder	10 Sep 2007 12:11:09 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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
>Index: files/patch-lib-scripts-fileindent
>===================================================================
>RCS file: files/patch-lib-scripts-fileindent
>diff -N files/patch-lib-scripts-fileindent
>--- files/patch-lib-scripts-fileindent	4 Apr 2008 12:15:22 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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 $
>- #
>Index: files/patch-lib-scripts-getsettings
>===================================================================
>RCS file: files/patch-lib-scripts-getsettings
>diff -N files/patch-lib-scripts-getsettings
>--- files/patch-lib-scripts-getsettings	4 Apr 2008 12:15:22 -0000	1.2
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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
>Index: files/patch-lib-scripts-patch_scripts.bash
>===================================================================
>RCS file: files/patch-lib-scripts-patch_scripts.bash
>diff -N files/patch-lib-scripts-patch_scripts.bash
>--- files/patch-lib-scripts-patch_scripts.bash	10 Sep 2007 12:11:09 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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
>Index: files/patch-lib-scripts-polyml_platform
>===================================================================
>RCS file: files/patch-lib-scripts-polyml_platform
>diff -N files/patch-lib-scripts-polyml_platform
>--- files/patch-lib-scripts-polyml_platform	4 Apr 2008 12:15:22 -0000	1.2
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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 $
>- #
>Index: files/patch-lib-scripts-polyml_version
>===================================================================
>RCS file: files/patch-lib-scripts-polyml_version
>diff -N files/patch-lib-scripts-polyml_version
>--- files/patch-lib-scripts-polyml_version	4 Apr 2008 12:15:22 -0000	1.2
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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 $
>- #
>Index: files/patch-lib-scripts-run_mosml
>===================================================================
>RCS file: files/patch-lib-scripts-run_mosml
>diff -N files/patch-lib-scripts-run_mosml
>--- files/patch-lib-scripts-run_mosml	10 Sep 2007 12:11:09 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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!
>- 
>Index: files/patch-lib-scripts-run_polyml
>===================================================================
>RCS file: files/patch-lib-scripts-run_polyml
>diff -N files/patch-lib-scripts-run_polyml
>--- files/patch-lib-scripts-run_polyml	4 Apr 2008 12:15:22 -0000	1.2
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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
>- 
>Index: files/patch-lib-scripts-run_polyml_5.0
>===================================================================
>RCS file: files/patch-lib-scripts-run_polyml_5.0
>diff -N files/patch-lib-scripts-run_polyml_5.0
>--- files/patch-lib-scripts-run_polyml_5.0	4 Apr 2008 12:15:22 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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
>- 
>Index: files/patch-lib-scripts-run_polyml_5.1
>===================================================================
>RCS file: files/patch-lib-scripts-run_polyml_5.1
>diff -N files/patch-lib-scripts-run_polyml_5.1
>--- files/patch-lib-scripts-run_polyml_5.1	4 Apr 2008 12:15:22 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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
>- 
>Index: files/patch-lib-scripts-run_poplogml
>===================================================================
>RCS file: files/patch-lib-scripts-run_poplogml
>diff -N files/patch-lib-scripts-run_poplogml
>--- files/patch-lib-scripts-run_poplogml	4 Apr 2008 12:15:22 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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
>- 
>Index: files/patch-lib-scripts-run_smlnj
>===================================================================
>RCS file: /home/ncvs/ports/math/isabelle/files/patch-lib-scripts-run_smlnj,v
>retrieving revision 1.2
>diff -u -r1.2 patch-lib-scripts-run_smlnj
>--- files/patch-lib-scripts-run_smlnj	4 Apr 2008 12:15:22 -0000	1.2
>+++ files/patch-lib-scripts-run_smlnj	29 Jul 2008 06:32:28 -0000
>@@ -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).
>- 
>--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 @@
>+--- 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 @@
>+ 
>  ## 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
>Index: files/patch-lib-scripts-timestart.bash
>===================================================================
>RCS file: files/patch-lib-scripts-timestart.bash
>diff -N files/patch-lib-scripts-timestart.bash
>--- files/patch-lib-scripts-timestart.bash	4 Apr 2008 12:15:22 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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"
>- }
>Index: files/patch-lib-scripts-timestop.bash
>===================================================================
>RCS file: files/patch-lib-scripts-timestop.bash
>diff -N files/patch-lib-scripts-timestop.bash
>--- files/patch-lib-scripts-timestop.bash	4 Apr 2008 12:15:22 -0000	1.1
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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"
>Index: files/patch-src-Pure-mk
>===================================================================
>RCS file: files/patch-src-Pure-mk
>diff -N files/patch-src-Pure-mk
>--- files/patch-src-Pure-mk	4 Apr 2008 12:15:22 -0000	1.2
>+++ /dev/null	1 Jan 1970 00:00:00 -0000
>@@ -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

Actions: View | Diff

Attachments on bug 126067: 89189