Date: Mon, 19 Oct 2009 08:39:33 +1100 (EST) From: Timothy Bourke <timbob@bigpond.com> To: FreeBSD-gnats-submit@FreeBSD.org Subject: ports/139737: [MAINTAINER] math/isabelle: update to 2009 Message-ID: <200910182139.n9ILdXa3014275@triptrop.cse.unsw.edu.au> Resent-Message-ID: <200910182200.n9IM0G7G047545@freefall.freebsd.org>
next in thread | raw e-mail | index | archive | help
>Number: 139737 >Category: ports >Synopsis: [MAINTAINER] math/isabelle: update to 2009 >Confidential: no >Severity: non-critical >Priority: low >Responsible: freebsd-ports-bugs >State: open >Quarter: >Keywords: >Date-Required: >Class: maintainer-update >Submitter-Id: current-users >Arrival-Date: Sun Oct 18 22:00:16 UTC 2009 >Closed-Date: >Last-Modified: >Originator: Timothy Bourke >Release: FreeBSD 6.4-RELEASE i386 >Organization: >Environment: System: FreeBSD triptrop 6.4-RELEASE FreeBSD 6.4-RELEASE #6: Sun Nov 30 20:46:29 EST 2008 >Description: - Update to 2009 Added file(s): - files/patch-src-HOL-Tools-atp_manager.ML - files/patch-src-HOL-Tools-atp_wrapper.ML - files/patch-src-HOL-Tools-int_arith.ML - files/patch-src-HOL-Tools-int_factor_simprocs.ML - files/patch-src-HOL-Tools-nat_simprocs.ML Generated with FreeBSD Port Tools 0.99 >How-To-Repeat: >Fix: --- isabelle-2009.patch begins here --- Index: Makefile =================================================================== RCS file: /home/ncvs/ports/math/isabelle/Makefile,v retrieving revision 1.10 diff -u -r1.10 Makefile --- Makefile 15 Aug 2008 04:33:03 -0000 1.10 +++ Makefile 18 Oct 2009 21:38:27 -0000 @@ -6,16 +6,16 @@ # PORTNAME= isabelle -PORTVERSION= 2008 +PORTVERSION= 2009 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= Isabelle2008 +DISTNAME= Isabelle2009 .if !defined(NOPORTDOCS) -DISTFILES= Isabelle2008.tar.gz \ - Isabelle2008_library.tar.gz \ - Isabelle2008_pdf.tar.gz +DISTFILES= Isabelle2009.tar.gz \ + Isabelle2009_library.tar.gz \ + Isabelle2009_pdf.tar.gz .endif MAINTAINER= timbob@bigpond.com @@ -25,15 +25,16 @@ 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_NSA "Build optional heap: HOL-NSA" 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 +USE_EMACS= yes # for EMACS_SITE_LISPDIR +EMACS_NO_BUILD_DEPENDS=yes +EMACS_NO_RUN_DEPENDS=yes BUILD_DEPENDS+= bash:${PORTSDIR}/shells/bash RUN_DEPENDS+= proofgeneral:${PORTSDIR}/math/proofgeneral RUN_DEPENDS+= bash:${PORTSDIR}/shells/bash @@ -56,44 +57,40 @@ .if defined(WITH_HOL_ALGEBRA) HEAP_HOL_ALGEBRA="" +EXTRA_HOL+=-m 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="" +EXTRA_HOL+=-m HOL-Nominal .else HEAP_HOL_NOMINAL="@comment " .endif +.if defined(WITH_HOL_NSA) +HEAP_HOL_NSA="" +EXTRA_HOL+=-m HOL-NSA +.else +HEAP_HOL_NSA="@comment " +.endif .if defined(WITH_HOL_WORD) HEAP_HOL_WORD="" +EXTRA_HOL+=-m HOL-Word .else HEAP_HOL_WORD="@comment " .endif .if defined(WITH_HOL_TLA) HEAP_HOL_TLA="" +EXTRA_HOL+=-m TLA .else HEAP_HOL_TLA="@comment " .endif .if defined(WITH_HOL_HOL4) HEAP_HOL_HOL4="" +EXTRA_HOL+=-m 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 @@ -107,21 +104,19 @@ .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_NSA=${HEAP_HOL_NSA} \ HEAP_HOL_WORD=${HEAP_HOL_WORD} \ HEAP_HOL_TLA=${HEAP_HOL_TLA} \ - HEAP_HOL_HOL4=${HEAP_HOL_HOL4} \ - HEAP_HOLCF_IOA=${HEAP_HOLCF_IOA} + HEAP_HOL_HOL4=${HEAP_HOL_HOL4} .if defined(WITH_SMLNJ) -BUILD_DEPENDS+= smlnj-devel>=110.65:${PORTSDIR}/lang/sml-nj-devel +BUILD_DEPENDS+= smlnj-devel>=110.71:${PORTSDIR}/lang/sml-nj-devel MAKE_ENV+= SMLNJ_DEVEL=yes .else -BUILD_DEPENDS+= polyml>=5.2:${PORTSDIR}/lang/polyml -RUN_DEPENDS+= polyml>=5.2:${PORTSDIR}/lang/polyml +BUILD_DEPENDS+= polyml>=5.2.1:${PORTSDIR}/lang/polyml +RUN_DEPENDS+= polyml>=5.2.1:${PORTSDIR}/lang/polyml .endif NO_INSTALL_MANPAGES=yes @@ -137,7 +132,10 @@ s|%%ML_DBASE%%|${ML_DBASE}|; \ s|%%ML_PLATFORM%%|${ML_PLATFORM}|; \ s|%%PREFIX%%|${PREFIX}|; \ - s|%%LINE_EDIT%%|${LINE_EDIT}|" \ + s|%%LINE_EDIT%%|${LINE_EDIT}|; \ + s|%%SYSTMPDIR%%|/tmp|; \ + s|%%JAVASHAREDIR%%|${PREFIX}/share/java|; \ + s|%%EMACS_SITE_LISPDIR%%|${EMACS_SITE_LISPDIR}|" \ ${WRKSRC}/etc/settings.presed > ${WRKSRC}/etc/settings @${RM} ${WRKSRC}/etc/settings.presed @${TOUCH} ${WRKSRC}/contrib/.keep @@ -145,33 +143,14 @@ ${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 +.if defined(EXTRA_HOL) + ${WRKSRC}/build -b ${EXTRA_HOL} HOL .endif post-install: - ${WRKSRC}/bin/isatool ${INSTALL} -d ${PREFIX}/share/isabelle -p ${PREFIX}/bin + ${WRKSRC}/bin/isabelle install \ + -d ${PREFIX}/share/isabelle \ + -p ${PREFIX}/bin .if !defined(NOPORTDOCS) ${MKDIR} ${DOCSDIR} .for file in ${DOCFILES} Index: distinfo =================================================================== RCS file: /home/ncvs/ports/math/isabelle/distinfo,v retrieving revision 1.5 diff -u -r1.5 distinfo --- distinfo 15 Aug 2008 04:33:03 -0000 1.5 +++ distinfo 18 Oct 2009 21:38:27 -0000 @@ -1,9 +1,9 @@ -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 +MD5 (Isabelle2009.tar.gz) = 2b7a8d49bfba64aac7227d692c15c27b +SHA256 (Isabelle2009.tar.gz) = 49f8708962a89102cd25d9b5b7bf1298017c0689f9ced7741c124351b58f8e71 +SIZE (Isabelle2009.tar.gz) = 9073615 +MD5 (Isabelle2009_library.tar.gz) = 8ffcb7a25a4d110dd9060d7fbb582fc6 +SHA256 (Isabelle2009_library.tar.gz) = db605638e4c66ed74069a4370cb6be776901e6ada6dfdd5104536379dbd0beef +SIZE (Isabelle2009_library.tar.gz) = 44856488 +MD5 (Isabelle2009_pdf.tar.gz) = 3e964988a4cb70d1589a8c89f1e3eac7 +SHA256 (Isabelle2009_pdf.tar.gz) = 0e451cabf1ece51cd989531dce14136b62c4138ace9bc618a1bd71d1c984ed70 +SIZE (Isabelle2009_pdf.tar.gz) = 5757069 Index: pkg-plist =================================================================== RCS file: /home/ncvs/ports/math/isabelle/pkg-plist,v retrieving revision 1.7 diff -u -r1.7 pkg-plist --- pkg-plist 15 Aug 2008 04:33:03 -0000 1.7 +++ pkg-plist 18 Oct 2009 21:38:29 -0000 @@ -1,9 +1,8 @@ -bin/Isabelle bin/isabelle -bin/isabelle-interface bin/isabelle-process -bin/isatool %%PORTDOCS%%%%DOCSDIR%%/Contents +%%PORTDOCS%%%%DOCSDIR%%/adaption.eps +%%PORTDOCS%%%%DOCSDIR%%/architecture.eps %%PORTDOCS%%%%DOCSDIR%%/browser_info/CCL/.session/entries %%PORTDOCS%%%%DOCSDIR%%/browser_info/CCL/.session/pre-index %%PORTDOCS%%%%DOCSDIR%%/browser_info/CCL/CCL.html @@ -61,8 +60,10 @@ %%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 @@ -81,7 +82,14 @@ %%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/atomize_elim.ML.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 @@ -89,13 +97,13 @@ %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/ex/Foundation.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/ex/GraphBrowser.jar %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/ex/If.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/ex/IffOracle.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/ex/Iff_Oracle.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/ex/Intro.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/ex/Intuitionistic.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/ex/LocaleTest.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/ex/Miniscope.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/ex/Nat.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/ex/NatClass.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/ex/Nat_Class.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/ex/Natural_Numbers.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/ex/Prolog.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOL/ex/Propositional_Cla.html @@ -110,47 +118,418 @@ %%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/intuitionistic.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/GraphBrowser.jar %%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/Classical.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/ex/Foundation.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/ex/GraphBrowser.jar %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/ex/If.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/ex/Intro.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/ex/Intuitionistic.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/ex/Nat.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/FOLP/ex/index.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/ex/isabelle.css %%PORTDOCS%%%%DOCSDIR%%/browser_info/FOLP/ex/large.html %%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-Base/.session/entries +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/.session/pre-index +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/Code_Setup.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/GraphBrowser.jar +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/HOL.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/README.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/atomize_elim.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/blast.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/clasimp.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/classical.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/code_funcgr.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/code_haskell.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/code_ml.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/code_name.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/code_printer.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/code_target.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/code_thingol.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/code_wellsorted.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/coherent.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/eqsubst.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/hologic.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/hypsubst.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/index.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/induct.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/induct_tacs.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/intuitionistic.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/isabelle.css +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/isand.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/large.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/medium.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/nbe.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/project_rule.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/quantifier1.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/random_word.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/recfun_codegen.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/rw_inst.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/rw_tools.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/session.graph +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/simpdata.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/small.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/splitter.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/value.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Base/zipper.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/.session/entries +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/.session/pre-index +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/ATP_Linkup.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Code_Eval.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Code_Message.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Code_Setup.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Datatype.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Divides.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Equiv_Relations.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Extraction.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Finite_Set.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Fun.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/FunDef.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/GraphBrowser.jar +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Groebner_Basis.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/HOL.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Hilbert_Choice.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Inductive.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Int.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/IntDiv.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Lattices.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/List.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Main.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Map.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Nat.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/NatBin.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Option.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/OrderedGroup.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Orderings.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Plain.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Power.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Predicate.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Presburger.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Product_Type.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/README.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Recdef.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Record.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Refute.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Relation.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Relation_Power.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Ring_and_Field.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/SAT.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Set.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/SetInterval.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Sum_Type.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Transitive_Closure.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Typedef.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Typerep.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/Wellfounded.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/abel_cancel.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/arith_data.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/assoc_fold.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/atomize_elim.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/atp_manager.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/atp_wrapper.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/auto_term.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/blast.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/cancel_div_mod.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/cancel_numeral_factor.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/cancel_numerals.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/cancel_sums.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/casesplit.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/clasimp.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/classical.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/cnf_funcs.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/code_funcgr.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/code_haskell.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/code_ml.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/code_name.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/code_printer.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/code_target.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/code_thingol.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/code_wellsorted.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/coherent.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/combine_numerals.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/context_tree.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/cooper.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/cooper_data.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/datatype_abs_proofs.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/datatype_aux.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/datatype_case.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/datatype_codegen.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/datatype_package.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/datatype_prop.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/datatype_realizer.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/datatype_rep_proofs.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/dcterm.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/decompose.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/descent.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/document.pdf +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/dseq.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/eqsubst.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/extract_common_term.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/fast_lin_arith.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/fundef_common.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/fundef_core.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/fundef_datatype.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/fundef_lib.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/fundef_package.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/generated_cooper.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/groebner.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/hologic.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/hypsubst.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/index.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/induct.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/induct_tacs.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/induction_scheme.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/inductive_codegen.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/inductive_package.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/inductive_realizer.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/inductive_set_package.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/inductive_wrap.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/int_arith.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/int_factor_simprocs.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/intuitionistic.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/isabelle.css +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/isand.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/large.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/lexicographic_order.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/lin_arith.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/measure_functions.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/medium.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/meson.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/metis.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/metis_tools.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/misc.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/mutual.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/nat_arith.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/nat_simprocs.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/nbe.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/normalizer.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/normalizer_data.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/numeral.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/numeral_syntax.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/old_primrec_package.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/order.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/outline.pdf +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/pattern_split.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/polyhash.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/post.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/presburger.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/primrec_package.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/project_rule.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/prop_logic.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/qelim.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/quantifier1.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/random_word.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/rat.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/recdef_package.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/recfun_codegen.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/record_package.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/refute.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/refute_isar.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/res_atp.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/res_axioms.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/res_clause.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/res_hol_clause.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/res_reconstruct.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/rewrite_hol_proof.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/rules.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/rw_inst.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/rw_tools.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/sat_funcs.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/sat_solver.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/scnp_reconstruct.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/scnp_solve.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/session.graph +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/simpdata.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/size.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/small.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/specification_package.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/split_rule.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/splitter.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/string_syntax.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/sum_tree.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/termination.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/tfl.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/thms.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/thry.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/trancl.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/typecopy_package.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/typedef_codegen.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/typedef_package.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/usyntax.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/utils.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/value.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Main/zipper.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/.session/entries +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/.session/pre-index +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/Code_Setup.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/Datatype.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/Divides.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/Extraction.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/Finite_Set.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/Fun.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/FunDef.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/GraphBrowser.jar +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/HOL.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/Inductive.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/Lattices.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/Nat.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/Option.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/OrderedGroup.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/Orderings.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/Plain.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/Power.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/Predicate.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/Product_Type.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/README.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/Record.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/Relation.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/Ring_and_Field.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/Set.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/Sum_Type.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/Transitive_Closure.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/Typedef.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/Wellfounded.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/abel_cancel.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/arith_data.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/atomize_elim.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/auto_term.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/blast.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/cancel_div_mod.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/cancel_sums.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/clasimp.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/classical.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/code_funcgr.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/code_haskell.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/code_ml.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/code_name.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/code_printer.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/code_target.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/code_thingol.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/code_wellsorted.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/coherent.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/context_tree.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/datatype_abs_proofs.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/datatype_aux.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/datatype_case.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/datatype_codegen.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/datatype_package.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/datatype_prop.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/datatype_realizer.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/datatype_rep_proofs.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/decompose.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/descent.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/document.pdf +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/dseq.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/eqsubst.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/fast_lin_arith.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/fundef_common.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/fundef_core.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/fundef_datatype.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/fundef_lib.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/fundef_package.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/hologic.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/hypsubst.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/index.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/induct.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/induct_tacs.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/induction_scheme.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/inductive_codegen.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/inductive_package.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/inductive_realizer.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/inductive_set_package.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/inductive_wrap.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/intuitionistic.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/isabelle.css +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/isand.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/large.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/lexicographic_order.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/lin_arith.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/measure_functions.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/medium.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/mutual.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/nat_arith.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/nbe.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/old_primrec_package.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/order.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/outline.pdf +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/pattern_split.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/primrec_package.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/project_rule.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/prop_logic.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/quantifier1.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/random_word.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/rat.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/recfun_codegen.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/record_package.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/rewrite_hol_proof.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/rw_inst.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/rw_tools.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/sat_solver.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/scnp_reconstruct.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/scnp_solve.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/session.graph +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/simpdata.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/size.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/small.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/split_rule.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/splitter.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/sum_tree.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/termination.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/trancl.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/typecopy_package.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/typedef_codegen.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/typedef_package.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/value.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL-Plain/zipper.ML.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/Arith_Tools.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Archimedean_Field.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Auth/.session/entries %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Auth/.session/pre-index %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Auth/Analz.html @@ -176,7 +555,7 @@ %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Auth/NS_Public.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Auth/NS_Public_Bad.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Auth/NS_Shared.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Auth/NatPair.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Auth/Nat_Int_Bij.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Auth/OtwayRees.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Auth/OtwayReesBella.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Auth/OtwayRees_AN.html @@ -205,19 +584,6 @@ %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Auth/outline.pdf %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Auth/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Auth/small.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/AxClasses/.session/entries -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/AxClasses/.session/pre-index -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/AxClasses/GraphBrowser.jar -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/AxClasses/Group.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/AxClasses/Product.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/AxClasses/README.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/AxClasses/Semigroups.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/AxClasses/index.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/AxClasses/isabelle.css -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/AxClasses/large.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/AxClasses/medium.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/AxClasses/session.graph -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/AxClasses/small.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Bali/.session/entries %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Bali/.session/pre-index %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Bali/AxCompl.html @@ -253,8 +619,44 @@ %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Bali/outline.pdf %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Bali/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Bali/small.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Code_Eval.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Code_Message.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Code_Setup.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Complex.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Complex_Main.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Datatype.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/.session/entries +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/.session/pre-index +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/Approximation.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/Approximation_Ex.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/Code_Index.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/Code_Integer.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/Cooper.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/Decision_Procs.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/Dense_Linear_Order.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/Dense_Linear_Order_Ex.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/Efficient_Nat.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/Ferrack.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/Float.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/GraphBrowser.jar +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/MIR.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/Reflection.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/cooper_tac.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/ferrack_tac.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/ferrante_rackoff.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/ferrante_rackoff_data.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/index.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/isabelle.css +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/langford.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/langford_data.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/large.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/medium.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/mir_tac.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/reflection.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/reify_data.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/session.graph +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Decision_Procs/small.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Deriv.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Divides.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Equiv_Relations.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Extraction.html @@ -265,7 +667,6 @@ %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Extraction/Efficient_Nat.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Extraction/Euclid.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Extraction/Factorization.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Extraction/GCD.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Extraction/GraphBrowser.jar %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Extraction/Greatest_Common_Divisor.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Extraction/Higman.html @@ -274,6 +675,8 @@ %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Extraction/Pigeonhole.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Extraction/Primes.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Extraction/QuotRem.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Extraction/Random.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Extraction/State_Monad.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Extraction/Util.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Extraction/Warshall.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Extraction/document.pdf @@ -284,9 +687,11 @@ %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Extraction/outline.pdf %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Extraction/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Extraction/small.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Fact.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Finite_Set.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Fun.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/FunDef.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/GCD.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/GraphBrowser.jar %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Groebner_Basis.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/.session/entries @@ -295,13 +700,14 @@ %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/Abstract.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/Bij.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/Binomial.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/Congruence.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/Coset.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/Divisibility.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/Exponent.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/Factor.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/Field.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/FiniteProduct.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/FuncSet.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/GCD.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/GraphBrowser.jar %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/Group.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/Ideal.html @@ -310,7 +716,9 @@ %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/Lattice.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/LongDiv.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/Module.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/Multiset.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/PID.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/Permutation.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/PolyHomo.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/Polynomial.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Algebra/Primes.html @@ -329,180 +737,44 @@ %%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 -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/.session/pre-index -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Abstract_Rat.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/CLim.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/CStar.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Complex.html -%%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/Fact.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Filter.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Float.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/GCD.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/GraphBrowser.jar -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HDeriv.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HLim.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HLog.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/.session/entries -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/.session/pre-index -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/ComputeHOL.html -%%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/FloatSparseMatrix.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.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/SparseMatrix.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/document.pdf -%%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/medium.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/outline.pdf -%%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 -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/.session/pre-index -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/GraphBrowser.jar -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/HOL4.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/HOL4Base.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/HOL4Compat.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/HOL4Prob.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/HOL4Real.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/HOL4Setup.html -%%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.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/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/medium.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/session.graph -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/small.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 -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HahnBanach/.session/entries -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HahnBanach/.session/pre-index -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HahnBanach/Bounds.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HahnBanach/FunctionNorm.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HahnBanach/FunctionOrder.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HahnBanach/GraphBrowser.jar -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HahnBanach/HahnBanach.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HahnBanach/HahnBanachExtLemmas.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HahnBanach/HahnBanachLemmas.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HahnBanach/HahnBanachSupLemmas.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HahnBanach/Linearform.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HahnBanach/NormedSpace.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HahnBanach/README.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HahnBanach/Subspace.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HahnBanach/VectorSpace.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HahnBanach/ZornLemma.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HahnBanach/document.pdf -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HahnBanach/index.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HahnBanach/isabelle.css -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HahnBanach/large.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HahnBanach/medium.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HahnBanach/outline.pdf -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HahnBanach/session.graph -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HahnBanach/small.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HyperDef.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/HyperNat.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Hyperreal.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/.session/entries -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/.session/pre-index -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/GraphBrowser.jar -%%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.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/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/medium.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/session.graph -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/small.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 -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Ln.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Log.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Lubs.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/MacLaurin.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/NSA.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/NSCA.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/NSComplex.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/NatStar.html -%%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/RComplete.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/README.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Rational.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Real.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/RealDef.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/RealPow.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/RealVector.html -%%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/StarDef.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Taylor.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Transcendental.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/Zorn.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/document.pdf -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/.session/entries -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/.session/pre-index -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/Arithmetic_Series_Complex.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/BigO.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/BigO_Complex.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/BinEx.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/Code_Index.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/Code_Integer.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/DenumRat.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/Efficient_Nat.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/Factorization.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/GraphBrowser.jar -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/HarmonicSeries.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/MIR.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/Multiset.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/NSPrimes.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/NatPair.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/Permutation.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/Primes.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/ReflectedFerrack.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/SetsAndFunctions.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/Sqrt.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/Sqrt_Script.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/document.pdf -%%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/medium.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/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/session.graph -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Complex/small.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/.session/entries +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/.session/pre-index +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/CLim.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/CStar.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/Filter.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/GraphBrowser.jar +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/HDeriv.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/HLim.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/HLog.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/HSEQ.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/HSeries.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/HTranscendental.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/HyperDef.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/HyperNat.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/Hypercomplex.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/Hyperreal.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/Infinite_Set.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/NSA.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/NSCA.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/NSComplex.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/NatStar.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/Order_Relation.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/Star.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/StarDef.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/Zorn.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/document.pdf +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/hypreal_arith.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/index.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/isabelle.css +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/large.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/medium.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/outline.pdf +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/session.graph +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/small.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-NSA/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 @@ -511,6 +783,7 @@ %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/Examples/CR_Takahashi.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/Examples/Class.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/Examples/Compile.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/Examples/Contexts.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/Examples/Crary.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/Examples/Fsub.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/Examples/GraphBrowser.jar @@ -520,7 +793,10 @@ %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/Examples/LocalWeakening.html %%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/Standardization.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/Examples/Support.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/Examples/VC_Condition.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Nominal/Examples/W.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 @@ -535,6 +811,15 @@ %%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_inductive2.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 @@ -555,17 +840,15 @@ %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Word/Examples/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Word/Examples/small.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Word/GraphBrowser.jar -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Word/Infinite_Set.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Word/Num_Lemmas.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Word/Numeral_Type.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Word/Parity.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Word/Size.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Word/TdThs.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Word/Word.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Word/WordArith.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Word/WordBitwise.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Word/WordDefinition.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Word/WordGenLib.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Word/WordMain.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Word/WordShift.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Word/document.pdf %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Word/index.html @@ -576,6 +859,70 @@ %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Word/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL-Word/small.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/.session/entries +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/.session/pre-index +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/ContNotDenum.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/GraphBrowser.jar +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/HOL4.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/HOL4Base.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/HOL4Compat.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/HOL4Prob.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/HOL4Real.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/HOL4Setup.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/HOL4Syntax.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/HOL4Vec.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/HOL4Word32.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/ImportRecorder.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/MakeEqual.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/Primes.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/README +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/hol4rews.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/import_package.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/import_syntax.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/importrecorder.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/index.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/isabelle.css +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/large.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/lazy_seq.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/medium.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/mono_scan.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/mono_seq.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/proof_kernel.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/replay.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/scan.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/seq.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/session.graph +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/shuffler.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/small.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/xml.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HOL4/xmlconv.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HahnBanach/.session/entries +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HahnBanach/.session/pre-index +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HahnBanach/Bounds.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HahnBanach/ContNotDenum.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HahnBanach/FunctionNorm.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HahnBanach/FunctionOrder.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HahnBanach/GraphBrowser.jar +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HahnBanach/HahnBanach.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HahnBanach/HahnBanachExtLemmas.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HahnBanach/HahnBanachLemmas.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HahnBanach/HahnBanachSupLemmas.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HahnBanach/Linearform.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HahnBanach/NormedSpace.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HahnBanach/Order_Relation.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HahnBanach/README.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HahnBanach/Subspace.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HahnBanach/VectorSpace.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HahnBanach/Zorn.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HahnBanach/ZornLemma.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HahnBanach/document.pdf +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HahnBanach/index.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HahnBanach/isabelle.css +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HahnBanach/large.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HahnBanach/medium.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HahnBanach/outline.pdf +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HahnBanach/session.graph +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/HahnBanach/small.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Hilbert_Choice.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Hoare/.session/entries %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Hoare/.session/pre-index @@ -596,6 +943,7 @@ %%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 @@ -639,6 +987,7 @@ %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/IMP/Expr.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/IMP/GraphBrowser.jar %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/IMP/Hoare.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/IMP/Live.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/IMP/Machines.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/IMP/Natural.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/IMP/Transition.html @@ -679,6 +1028,61 @@ %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/IOA/medium.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/IOA/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/IOA/small.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Imperative_HOL/.session/entries +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Imperative_HOL/.session/pre-index +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Imperative_HOL/Array.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Imperative_HOL/Code_Index.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Imperative_HOL/Code_Integer.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Imperative_HOL/Countable.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Imperative_HOL/Efficient_Nat.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Imperative_HOL/GraphBrowser.jar +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Imperative_HOL/Heap.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Imperative_HOL/Heap_Monad.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Imperative_HOL/Imperative_HOL.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Imperative_HOL/Imperative_HOL_ex.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Imperative_HOL/Imperative_Quicksort.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Imperative_HOL/Multiset.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Imperative_HOL/Nat_Int_Bij.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Imperative_HOL/Ref.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Imperative_HOL/Relational.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Imperative_HOL/Subarray.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Imperative_HOL/Sublist.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Imperative_HOL/index.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Imperative_HOL/isabelle.css +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Imperative_HOL/large.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Imperative_HOL/medium.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Imperative_HOL/session.graph +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Imperative_HOL/small.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/.session/entries +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/.session/pre-index +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/ContNotDenum.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/GraphBrowser.jar +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/HOL4Compat.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/HOL4Setup.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/HOL4Syntax.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/ImportRecorder.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/MakeEqual.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/Primes.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/hol4rews.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/import_package.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/import_syntax.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/importrecorder.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/index.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/isabelle.css +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/large.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/lazy_seq.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/medium.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/mono_scan.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/mono_seq.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/proof_kernel.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/replay.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/scan.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/seq.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/session.graph +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/shuffler.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/small.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/xml.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Import/xmlconv.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Induct/.session/entries %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Induct/.session/pre-index %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Induct/ABexp.html @@ -688,7 +1092,6 @@ %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Induct/GraphBrowser.jar %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Induct/LFilter.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Induct/LList.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Induct/Mutil.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Induct/Ordinals.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Induct/PropLog.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Induct/QuoDataType.html @@ -708,7 +1111,9 @@ %%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/Int.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/IntDiv.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Integration.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Isar_examples/.session/entries %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Isar_examples/.session/pre-index %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Isar_examples/BasicLogic.html @@ -716,12 +1121,12 @@ %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Isar_examples/Drinker.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Isar_examples/ExprCompiler.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Isar_examples/Fibonacci.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Isar_examples/GCD.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Isar_examples/GraphBrowser.jar %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Isar_examples/Group.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Isar_examples/Hoare.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Isar_examples/HoareEx.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Isar_examples/KnasterTarski.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Isar_examples/Lattice_Syntax.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Isar_examples/MutilatedCheckerboard.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Isar_examples/NestedDatatype.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Isar_examples/Peirce.html @@ -730,6 +1135,7 @@ %%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 @@ -785,6 +1191,7 @@ %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/AssocList.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/BigO.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Binomial.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Bit.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Boolean_Algebra.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Char_nat.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Char_ord.html @@ -792,63 +1199,144 @@ %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Code_Char_chr.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Code_Index.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Code_Integer.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Code_Message.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Coinductive_List.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Commutative_Ring.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/ContNotDenum.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Continuity.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/Determinants.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Diagonalize.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Efficient_Nat.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Enum.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Euclidean_Space.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Eval_Witness.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Executable_Set.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Finite_Cartesian_Product.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Float.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Formal_Power_Series.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/FrechetDeriv.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/FuncSet.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/GCD.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Fundamental_Theorem_Algebra.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Glbs.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/GraphBrowser.jar %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Infinite_Set.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Inner_Product.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/LaTeXsugar.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Lattice_Syntax.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Library.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/ListVector.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/List_Prefix.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/List_lexord.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Mapping.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Multiset.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/NatPair.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Nat_Infinity.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Nat_Int_Bij.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Nested_Environment.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Numeral_Type.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Option_ord.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/OptionalSugar.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Parity.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Order_Relation.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Permutation.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Permutations.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Pocklington.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Poly_Deriv.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Polynomial.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Primes.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Product_Vector.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Product_ord.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Product_plus.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Quickcheck.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Quicksort.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Quotient.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/RBT.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Ramsey.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Random.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Reflection.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/SetsAndFunctions.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/State_Monad.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Sublist_Order.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Topology_Euclidean_Space.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/Univ_Poly.html %%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/ferrante_rackoff.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/ferrante_rackoff_data.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/index.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/isabelle.css +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/langford.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/langford_data.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/large.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/medium.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/normarith.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/outline.pdf +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/reflection.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/reify_data.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Library/small.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Lim.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/List.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Ln.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Log.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Lubs.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MacLaurin.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Main.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Map.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/.session/entries +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/.session/pre-index +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/ComputeFloat.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/ComputeHOL.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/ComputeNumeral.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/Compute_Oracle.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/Cplex.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/CplexMatrixConverter.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/Cplex_tools.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/FloatSparseMatrixBuilder.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/GraphBrowser.jar +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/LP.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/Matrix.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/SparseMatrix.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/am.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/am_compiler.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/am_ghc.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/am_interpreter.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/am_sml.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/compute.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/document.pdf +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/float.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/float_arith.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/fspmlp.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/index.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/isabelle.css +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/large.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/linker.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/matrixlp.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/medium.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/outline.pdf +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/report.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/session.graph +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Matrix/small.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MetisExamples/.session/entries %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MetisExamples/.session/pre-index %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MetisExamples/Abstraction.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MetisExamples/BT.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MetisExamples/BigO.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MetisExamples/Dense_Linear_Order.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MetisExamples/FuncSet.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MetisExamples/GraphBrowser.jar %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MetisExamples/Message.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MetisExamples/SetsAndFunctions.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MetisExamples/Tarski.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MetisExamples/TransClosure.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MetisExamples/ferrante_rackoff.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MetisExamples/ferrante_rackoff_data.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MetisExamples/index.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MetisExamples/isabelle.css +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MetisExamples/langford.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MetisExamples/langford_data.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MetisExamples/large.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MetisExamples/medium.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MetisExamples/session.graph @@ -896,6 +1384,7 @@ %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MicroJava/LBVSpec.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MicroJava/LemmasComp.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MicroJava/Listn.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MicroJava/MicroJava.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MicroJava/Opt.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MicroJava/Product.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/MicroJava/Semilat.html @@ -935,6 +1424,7 @@ %%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 @@ -958,6 +1448,7 @@ %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/NanoJava/small.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Nat.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/NatBin.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/NthRoot.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/NumberTheory/.session/entries %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/NumberTheory/.session/pre-index %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/NumberTheory/BijectionRel.html @@ -968,7 +1459,6 @@ %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/NumberTheory/Factorization.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/NumberTheory/Fib.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/NumberTheory/Finite2.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/NumberTheory/GCD.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/NumberTheory/Gauss.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/NumberTheory/GraphBrowser.jar %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/NumberTheory/Infinite_Set.html @@ -990,8 +1480,12 @@ %%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/Option.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/OrderedGroup.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Orderings.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/PReal.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Parity.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Plain.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Power.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Predicate.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Presburger.html @@ -1008,9 +1502,16 @@ %%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/RComplete.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/README.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Rational.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Real.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/RealDef.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/RealPow.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/RealVector.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Recdef.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Record.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Refute.html @@ -1018,6 +1519,7 @@ %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Relation_Power.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Ring_and_Field.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/SAT.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/SEQ.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/SET-Protocol/.session/entries %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/SET-Protocol/.session/pre-index %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/SET-Protocol/Cardholder_Registration.html @@ -1025,7 +1527,7 @@ %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/SET-Protocol/GraphBrowser.jar %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/SET-Protocol/Merchant_Registration.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/SET-Protocol/MessageSET.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/SET-Protocol/NatPair.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/SET-Protocol/Nat_Int_Bij.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/SET-Protocol/PublicSET.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/SET-Protocol/Purchase.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/SET-Protocol/document.pdf @@ -1036,6 +1538,7 @@ %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/SET-Protocol/outline.pdf %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/SET-Protocol/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/SET-Protocol/small.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Series.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Set.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/SetInterval.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/SizeChange/.session/entries @@ -1058,6 +1561,7 @@ %%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 @@ -1068,6 +1572,7 @@ %%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 @@ -1076,6 +1581,8 @@ %%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 @@ -1145,8 +1652,11 @@ %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/TLA/medium.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/TLA/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/TLA/small.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Taylor.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Transcendental.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Transitive_Closure.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Typedef.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/Typerep.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/UNITY/.session/entries %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/UNITY/.session/pre-index %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/UNITY/Alloc.html @@ -1180,6 +1690,7 @@ %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/UNITY/PPROD.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/UNITY/Priority.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/UNITY/PriorityAux.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/UNITY/Progress.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/UNITY/ProgressSets.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/UNITY/Project.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/UNITY/Public.html @@ -1193,6 +1704,7 @@ %%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 @@ -1230,6 +1742,7 @@ %%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.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 @@ -1248,14 +1761,56 @@ %%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/atomize_elim.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/atp_manager.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/atp_wrapper.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_haskell.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/code_ml.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/code_name.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/code_printer.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/code_wellsorted.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/coherent.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/decompose.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/descent.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 -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Abstract_Rat.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Adder.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Antiquote.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Arith_Examples.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Arithmetic_Series_Complex.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/AssocList.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/BT.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/BinEx.html @@ -1264,138 +1819,214 @@ %%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/Code_Char.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 %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Codegenerator.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Codegenerator_Pretty.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Coherent.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Commutative_Ring.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Commutative_RingEx.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Commutative_Ring_Complete.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Dense_Linear_Order_Ex.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Efficient_Nat.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Eval.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/Eval_Examples.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/ExecutableContent.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Factorization.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Formal_Power_Series.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Formal_Power_Series_Examples.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 %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/GraphBrowser.jar %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Groebner_Examples.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Guess.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/HarmonicSeries.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Hebrew.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Hex_Bin_Examples.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Higher_Order_Logic.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Hilbert_Classical.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Induction_Scheme.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/InductiveInvariant.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/InductiveInvariant_examples.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Intuitionistic.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/LaTeXsugar.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Lagrange.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Lattice_Syntax.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/List_Prefix.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/LocaleTest2.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Locales.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/MT.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/MergeSort.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Meson_Test.html %%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/NatPair.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/NatSum.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Nat_Infinity.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Nested_Environment.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/NormalForm.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Numeral.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Option_ord.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/PER.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/PReal.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Parity.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Permutation.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Predicate_Compile.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/PresburgerEx.html %%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/Puzzle.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Quickcheck.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Quickcheck_Examples.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Quickcheck_Generators.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/README.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Random.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Rational.html -%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/RealDef.html %%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.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/ReflectionEx.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Refute_Examples.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/SAT_Examples.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/SVC_Oracle.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Serbian.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/SetsAndFunctions.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Sorting.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Sqrt.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Sqrt_Script.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/State_Monad.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Tarski.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Term_Of_Syntax.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/Termination.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/ThreeDivides.html %%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/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/predicate_compile.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/reflection.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/ex/reify_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/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/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/float_syntax.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/index.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/induct.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/induct_tacs.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/induction_scheme.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_arith.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/int_factor_simprocs.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/intuitionistic.ML.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/isabelle.css +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/isand.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/measure_functions.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_arith.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/old_primrec_package.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/random_word.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/rat.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/rat_arith.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/real_arith.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_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/scnp_reconstruct.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/scnp_solve.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/sum_tree.ML.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOL/termination.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/value.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 +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Algebraic.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Bifinite.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Cfun.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/CompactBasis.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Completion.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Cont.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/ConvexPD.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Countable.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Cprod.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Deflation.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Discrete.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Domain.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Eventual.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/FOCUS/.session/entries %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/FOCUS/.session/pre-index %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/FOCUS/Buffer.html @@ -1480,6 +2111,7 @@ %%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 @@ -1538,22 +2170,39 @@ %%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 %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/IOA/session.graph %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/IOA/small.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Infinite_Set.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Lift.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/LowerPD.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/NatIso.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Nat_Int_Bij.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/One.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Pcpo.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Pcpodef.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Porder.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Product_Cpo.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/README.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Sprod.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Ssum.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Sum_Cpo.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Tr.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Universal.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/Up.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/UpperPD.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 @@ -1565,6 +2214,7 @@ %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/ex/Hoare.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/ex/Loop.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/ex/Nat_Infinity.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/ex/Powerdomain_ex.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/ex/Stream.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/ex/index.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/HOLCF/ex/isabelle.css @@ -1572,20 +2222,16 @@ %%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 @@ -1651,7 +2297,10 @@ %%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 @@ -1737,6 +2386,7 @@ %%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_ZF.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Epsilon.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/EquivClass.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Finite.html @@ -1783,10 +2433,16 @@ %%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_ZF.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/InfDatatype.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/IntArith.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/IntDiv_ZF.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Int_ZF.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/List_ZF.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Main.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Main_ZF.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Main_ZFC.html +%%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Nat_ZF.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/OrdQuant.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/Order.html %%PORTDOCS%%%%DOCSDIR%%/browser_info/ZF/OrderArith.html @@ -1849,6 +2505,11 @@ %%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 @@ -1873,22 +2534,24 @@ %%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 @@ -1896,13 +2559,14 @@ %%PORTDOCS%%%%DOCSDIR%%/classes.pdf %%PORTDOCS%%%%DOCSDIR%%/codegen.dvi %%PORTDOCS%%%%DOCSDIR%%/codegen.pdf -%%PORTDOCS%%%%DOCSDIR%%/codegen_process.ps %%PORTDOCS%%%%DOCSDIR%%/functions.dvi %%PORTDOCS%%%%DOCSDIR%%/functions.pdf %%PORTDOCS%%%%DOCSDIR%%/implementation.dvi %%PORTDOCS%%%%DOCSDIR%%/implementation.pdf %%PORTDOCS%%%%DOCSDIR%%/ind-defs.dvi %%PORTDOCS%%%%DOCSDIR%%/ind-defs.pdf +%%PORTDOCS%%%%DOCSDIR%%/intro.dvi +%%PORTDOCS%%%%DOCSDIR%%/intro.pdf %%PORTDOCS%%%%DOCSDIR%%/isabelle.eps %%PORTDOCS%%%%DOCSDIR%%/isabelle_hol.eps %%PORTDOCS%%%%DOCSDIR%%/isabelle_isar.eps @@ -1911,6 +2575,8 @@ %%PORTDOCS%%%%DOCSDIR%%/isar-overview.pdf %%PORTDOCS%%%%DOCSDIR%%/isar-ref.dvi %%PORTDOCS%%%%DOCSDIR%%/isar-ref.pdf +%%PORTDOCS%%%%DOCSDIR%%/isar-vm.eps +%%PORTDOCS%%%%DOCSDIR%%/isar-vm.pdf %%PORTDOCS%%%%DOCSDIR%%/locales.dvi %%PORTDOCS%%%%DOCSDIR%%/locales.pdf %%PORTDOCS%%%%DOCSDIR%%/logics-HOL.dvi @@ -1919,6 +2585,8 @@ %%PORTDOCS%%%%DOCSDIR%%/logics-ZF.pdf %%PORTDOCS%%%%DOCSDIR%%/logics.dvi %%PORTDOCS%%%%DOCSDIR%%/logics.pdf +%%PORTDOCS%%%%DOCSDIR%%/main.dvi +%%PORTDOCS%%%%DOCSDIR%%/main.pdf %%PORTDOCS%%%%DOCSDIR%%/pghead.eps %%PORTDOCS%%%%DOCSDIR%%/ref.dvi %%PORTDOCS%%%%DOCSDIR%%/ref.pdf @@ -1934,72 +2602,50 @@ %%DATADIR%%/COPYRIGHT %%DATADIR%%/NEWS %%DATADIR%%/README -%%DATADIR%%/bin/Isabelle %%DATADIR%%/bin/isabelle -%%DATADIR%%/bin/isabelle-interface %%DATADIR%%/bin/isabelle-process -%%DATADIR%%/bin/isatool %%DATADIR%%/build %%DATADIR%%/contrib/.keep +%%DATADIR%%/contrib/SystemOnTPTP/remote %%DATADIR%%/etc/isar-keywords-ZF.el %%DATADIR%%/etc/isar-keywords.el %%DATADIR%%/etc/proofgeneral-settings.el %%DATADIR%%/etc/settings +%%DATADIR%%/etc/symbols %%DATADIR%%/etc/user-settings.sample %%DATADIR%%/heaps/%%HEAPSUBDIR%%/CCL %%DATADIR%%/heaps/%%HEAPSUBDIR%%/CTT %%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 %%DATADIR%%/heaps/%%HEAPSUBDIR%%/ZF +%%HEAP_HOL_ALGEBRA%%%%DATADIR%%/heaps/%%HEAPSUBDIR%%/HOL-Algebra +%%HEAP_HOL_NOMINAL%%%%DATADIR%%/heaps/%%HEAPSUBDIR%%/HOL-Nominal +%%HEAP_HOL_NSA%%%%DATADIR%%/heaps/%%HEAPSUBDIR%%/HOL-NSA +%%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%%/log/CCL.gz %%DATADIR%%/heaps/%%HEAPSUBDIR%%/log/CTT.gz %%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 +%%HEAP_HOL_ALGEBRA%%%%DATADIR%%/heaps/%%HEAPSUBDIR%%/log/HOL-Algebra.gz +%%HEAP_HOL_NOMINAL%%%%DATADIR%%/heaps/%%HEAPSUBDIR%%/log/HOL-Nominal.gz +%%HEAP_HOL_NSA%%%%DATADIR%%/heaps/%%HEAPSUBDIR%%/log/HOL-NSA.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%%/lib/ProofGeneral/README %%DATADIR%%/lib/ProofGeneral/pgip.rnc %%DATADIR%%/lib/ProofGeneral/pgip_isar.xml @@ -2007,28 +2653,33 @@ %%DATADIR%%/lib/ProofGeneral/schemas.xml %%DATADIR%%/lib/Tools/browser %%DATADIR%%/lib/Tools/codegen -%%DATADIR%%/lib/Tools/convert %%DATADIR%%/lib/Tools/dimacs2hol %%DATADIR%%/lib/Tools/display %%DATADIR%%/lib/Tools/doc %%DATADIR%%/lib/Tools/document +%%DATADIR%%/lib/Tools/emacs +%%DATADIR%%/lib/Tools/env %%DATADIR%%/lib/Tools/findlogics -%%DATADIR%%/lib/Tools/fixheaders %%DATADIR%%/lib/Tools/getenv %%DATADIR%%/lib/Tools/install +%%DATADIR%%/lib/Tools/java +%%DATADIR%%/lib/Tools/jedit %%DATADIR%%/lib/Tools/keywords %%DATADIR%%/lib/Tools/latex %%DATADIR%%/lib/Tools/logo %%DATADIR%%/lib/Tools/make %%DATADIR%%/lib/Tools/makeall %%DATADIR%%/lib/Tools/mkdir +%%DATADIR%%/lib/Tools/mkfifo %%DATADIR%%/lib/Tools/mkproject %%DATADIR%%/lib/Tools/print +%%DATADIR%%/lib/Tools/rmfifo +%%DATADIR%%/lib/Tools/scala %%DATADIR%%/lib/Tools/tty -%%DATADIR%%/lib/Tools/yxml %%DATADIR%%/lib/Tools/unsymbolize %%DATADIR%%/lib/Tools/usedir %%DATADIR%%/lib/Tools/version +%%DATADIR%%/lib/Tools/yxml %%DATADIR%%/lib/browser/GraphBrowser.jar %%DATADIR%%/lib/browser/GraphBrowser/AWTFontMetrics.java %%DATADIR%%/lib/browser/GraphBrowser/AbstractFontMetrics.java @@ -2052,6 +2703,14 @@ %%DATADIR%%/lib/browser/awtUtilities/Border.java %%DATADIR%%/lib/browser/awtUtilities/MessageDialog.java %%DATADIR%%/lib/browser/awtUtilities/TextFrame.java +%%DATADIR%%/lib/classes/Pure.jar +%%DATADIR%%/lib/fonts/IsabelleItalic.sfd +%%DATADIR%%/lib/fonts/IsabelleItalic.ttf +%%DATADIR%%/lib/fonts/IsabelleMono.sfd +%%DATADIR%%/lib/fonts/IsabelleMono.ttf +%%DATADIR%%/lib/fonts/IsabelleMonoBold.sfd +%%DATADIR%%/lib/fonts/IsabelleMonoBold.ttf +%%DATADIR%%/lib/fonts/README %%DATADIR%%/lib/html/isabelle.css %%DATADIR%%/lib/html/library_index_content.template %%DATADIR%%/lib/html/library_index_footer.template @@ -2060,6 +2719,13 @@ %%DATADIR%%/lib/icons/isabelle.xpm %%DATADIR%%/lib/jedit/README %%DATADIR%%/lib/jedit/isabelle.xml +%%DATADIR%%/lib/jedit/plugin/Isabelle.props +%%DATADIR%%/lib/jedit/plugin/dockables.xml +%%DATADIR%%/lib/jedit/plugin/isabelle_dock.scala +%%DATADIR%%/lib/jedit/plugin/isabelle_parser.scala +%%DATADIR%%/lib/jedit/plugin/isabelle_plugin.scala +%%DATADIR%%/lib/jedit/plugin/mk +%%DATADIR%%/lib/jedit/plugin/services.xml %%DATADIR%%/lib/logo/index.html %%DATADIR%%/lib/logo/isabelle-small.xpm %%DATADIR%%/lib/logo/isabelle-tiny.xpm @@ -2073,24 +2739,26 @@ %%DATADIR%%/lib/logo/isabelle_transparent.gif %%DATADIR%%/lib/logo/isabelle_zf.eps %%DATADIR%%/lib/logo/isabelle_zf.gif -%%DATADIR%%/lib/scripts/convert.pl %%DATADIR%%/lib/scripts/dimacs2hol.pl %%DATADIR%%/lib/scripts/feeder %%DATADIR%%/lib/scripts/feeder.pl %%DATADIR%%/lib/scripts/fileident -%%DATADIR%%/lib/scripts/fixheaders.pl %%DATADIR%%/lib/scripts/getsettings %%DATADIR%%/lib/scripts/keywords.pl %%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-4.1.3 +%%DATADIR%%/lib/scripts/run-polyml-4.1.4 +%%DATADIR%%/lib/scripts/run-polyml-4.2.0 %%DATADIR%%/lib/scripts/run-polyml-5.0 -%%DATADIR%%/lib/scripts/run-poplogml %%DATADIR%%/lib/scripts/run-smlnj +%%DATADIR%%/lib/scripts/system.pl %%DATADIR%%/lib/scripts/timestart.bash %%DATADIR%%/lib/scripts/timestop.bash %%DATADIR%%/lib/scripts/unsymbolize.pl +%%DATADIR%%/lib/scripts/yxml.pl %%DATADIR%%/lib/texinputs/draft.tex %%DATADIR%%/lib/texinputs/isabelle.sty %%DATADIR%%/lib/texinputs/isabellesym.sty @@ -2142,13 +2810,13 @@ %%DATADIR%%/src/FOL/ex/First_Order_Logic.thy %%DATADIR%%/src/FOL/ex/Foundation.thy %%DATADIR%%/src/FOL/ex/If.thy -%%DATADIR%%/src/FOL/ex/IffOracle.thy +%%DATADIR%%/src/FOL/ex/Iff_Oracle.thy %%DATADIR%%/src/FOL/ex/Intro.thy %%DATADIR%%/src/FOL/ex/Intuitionistic.thy %%DATADIR%%/src/FOL/ex/LocaleTest.thy %%DATADIR%%/src/FOL/ex/Miniscope.thy %%DATADIR%%/src/FOL/ex/Nat.thy -%%DATADIR%%/src/FOL/ex/NatClass.thy +%%DATADIR%%/src/FOL/ex/Nat_Class.thy %%DATADIR%%/src/FOL/ex/Natural_Numbers.thy %%DATADIR%%/src/FOL/ex/Prolog.thy %%DATADIR%%/src/FOL/ex/Propositional_Cla.thy @@ -2166,19 +2834,19 @@ %%DATADIR%%/src/FOLP/IsaMakefile %%DATADIR%%/src/FOLP/ROOT.ML %%DATADIR%%/src/FOLP/classical.ML -%%DATADIR%%/src/FOLP/ex/If.thy -%%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/Classical.thy %%DATADIR%%/src/FOLP/ex/Foundation.thy +%%DATADIR%%/src/FOLP/ex/If.thy %%DATADIR%%/src/FOLP/ex/Intro.thy %%DATADIR%%/src/FOLP/ex/Intuitionistic.thy +%%DATADIR%%/src/FOLP/ex/Nat.thy +%%DATADIR%%/src/FOLP/ex/Prolog.ML +%%DATADIR%%/src/FOLP/ex/Prolog.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/ex/ROOT.ML %%DATADIR%%/src/FOLP/hypsubst.ML %%DATADIR%%/src/FOLP/intprover.ML %%DATADIR%%/src/FOLP/simp.ML @@ -2186,7 +2854,9 @@ %%DATADIR%%/src/HOL/ATP_Linkup.thy %%DATADIR%%/src/HOL/Algebra/AbelCoset.thy %%DATADIR%%/src/HOL/Algebra/Bij.thy +%%DATADIR%%/src/HOL/Algebra/Congruence.thy %%DATADIR%%/src/HOL/Algebra/Coset.thy +%%DATADIR%%/src/HOL/Algebra/Divisibility.thy %%DATADIR%%/src/HOL/Algebra/Exponent.thy %%DATADIR%%/src/HOL/Algebra/FiniteProduct.thy %%DATADIR%%/src/HOL/Algebra/Group.thy @@ -2215,37 +2885,7 @@ %%DATADIR%%/src/HOL/Algebra/poly/Polynomial.thy %%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/Archimedean_Field.thy %%DATADIR%%/src/HOL/Auth/CertifiedEmail.thy %%DATADIR%%/src/HOL/Auth/Event.thy %%DATADIR%%/src/HOL/Auth/Guard/Analz.thy @@ -2291,12 +2931,6 @@ %%DATADIR%%/src/HOL/Auth/Yahalom_Bad.thy %%DATADIR%%/src/HOL/Auth/ZhouGollmann.thy %%DATADIR%%/src/HOL/Auth/document/root.tex -%%DATADIR%%/src/HOL/AxClasses/Group.thy -%%DATADIR%%/src/HOL/AxClasses/Lattice/OrdInsts.thy -%%DATADIR%%/src/HOL/AxClasses/Product.thy -%%DATADIR%%/src/HOL/AxClasses/README.html -%%DATADIR%%/src/HOL/AxClasses/ROOT.ML -%%DATADIR%%/src/HOL/AxClasses/Semigroups.thy %%DATADIR%%/src/HOL/Bali/AxCompl.thy %%DATADIR%%/src/HOL/Bali/AxExample.thy %%DATADIR%%/src/HOL/Bali/AxSem.thy @@ -2323,34 +2957,25 @@ %%DATADIR%%/src/HOL/Bali/WellForm.thy %%DATADIR%%/src/HOL/Bali/WellType.thy %%DATADIR%%/src/HOL/Bali/document/root.tex +%%DATADIR%%/src/HOL/Code_Eval.thy +%%DATADIR%%/src/HOL/Code_Message.thy %%DATADIR%%/src/HOL/Code_Setup.thy -%%DATADIR%%/src/HOL/Complex/CLim.thy -%%DATADIR%%/src/HOL/Complex/CStar.thy -%%DATADIR%%/src/HOL/Complex/Complex.thy -%%DATADIR%%/src/HOL/Complex/Complex_Main.thy -%%DATADIR%%/src/HOL/Complex/NSCA.thy -%%DATADIR%%/src/HOL/Complex/NSComplex.thy -%%DATADIR%%/src/HOL/Complex/README.html -%%DATADIR%%/src/HOL/Complex/ROOT.ML -%%DATADIR%%/src/HOL/Complex/document/root.tex -%%DATADIR%%/src/HOL/Complex/ex/Arithmetic_Series_Complex.thy -%%DATADIR%%/src/HOL/Complex/ex/BigO_Complex.thy -%%DATADIR%%/src/HOL/Complex/ex/BinEx.thy -%%DATADIR%%/src/HOL/Complex/ex/DenumRat.thy -%%DATADIR%%/src/HOL/Complex/ex/HarmonicSeries.thy -%%DATADIR%%/src/HOL/Complex/ex/MIR.thy -%%DATADIR%%/src/HOL/Complex/ex/NSPrimes.thy -%%DATADIR%%/src/HOL/Complex/ex/ROOT.ML -%%DATADIR%%/src/HOL/Complex/ex/ReflectedFerrack.thy -%%DATADIR%%/src/HOL/Complex/ex/Sqrt.thy -%%DATADIR%%/src/HOL/Complex/ex/Sqrt_Script.thy -%%DATADIR%%/src/HOL/Complex/ex/document/root.tex -%%DATADIR%%/src/HOL/Complex/ex/linreif.ML -%%DATADIR%%/src/HOL/Complex/ex/linrtac.ML -%%DATADIR%%/src/HOL/Complex/ex/mireif.ML -%%DATADIR%%/src/HOL/Complex/ex/mirtac.ML +%%DATADIR%%/src/HOL/Complex.thy +%%DATADIR%%/src/HOL/Complex_Main.thy %%DATADIR%%/src/HOL/Datatype.thy -%%DATADIR%%/src/HOL/Dense_Linear_Order.thy +%%DATADIR%%/src/HOL/Decision_Procs/Approximation.thy +%%DATADIR%%/src/HOL/Decision_Procs/Cooper.thy +%%DATADIR%%/src/HOL/Decision_Procs/Decision_Procs.thy +%%DATADIR%%/src/HOL/Decision_Procs/Dense_Linear_Order.thy +%%DATADIR%%/src/HOL/Decision_Procs/Ferrack.thy +%%DATADIR%%/src/HOL/Decision_Procs/MIR.thy +%%DATADIR%%/src/HOL/Decision_Procs/ROOT.ML +%%DATADIR%%/src/HOL/Decision_Procs/cooper_tac.ML +%%DATADIR%%/src/HOL/Decision_Procs/ex/Approximation_Ex.thy +%%DATADIR%%/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy +%%DATADIR%%/src/HOL/Decision_Procs/ferrack_tac.ML +%%DATADIR%%/src/HOL/Decision_Procs/mir_tac.ML +%%DATADIR%%/src/HOL/Deriv.thy %%DATADIR%%/src/HOL/Divides.thy %%DATADIR%%/src/HOL/Equiv_Relations.thy %%DATADIR%%/src/HOL/Extraction.thy @@ -2364,11 +2989,29 @@ %%DATADIR%%/src/HOL/Extraction/Warshall.thy %%DATADIR%%/src/HOL/Extraction/document/root.bib %%DATADIR%%/src/HOL/Extraction/document/root.tex +%%DATADIR%%/src/HOL/Fact.thy %%DATADIR%%/src/HOL/Finite_Set.thy %%DATADIR%%/src/HOL/Fun.thy %%DATADIR%%/src/HOL/FunDef.thy +%%DATADIR%%/src/HOL/GCD.thy %%DATADIR%%/src/HOL/Groebner_Basis.thy %%DATADIR%%/src/HOL/HOL.thy +%%DATADIR%%/src/HOL/HahnBanach/Bounds.thy +%%DATADIR%%/src/HOL/HahnBanach/FunctionNorm.thy +%%DATADIR%%/src/HOL/HahnBanach/FunctionOrder.thy +%%DATADIR%%/src/HOL/HahnBanach/HahnBanach.thy +%%DATADIR%%/src/HOL/HahnBanach/HahnBanachExtLemmas.thy +%%DATADIR%%/src/HOL/HahnBanach/HahnBanachLemmas.thy +%%DATADIR%%/src/HOL/HahnBanach/HahnBanachSupLemmas.thy +%%DATADIR%%/src/HOL/HahnBanach/Linearform.thy +%%DATADIR%%/src/HOL/HahnBanach/NormedSpace.thy +%%DATADIR%%/src/HOL/HahnBanach/README.html +%%DATADIR%%/src/HOL/HahnBanach/ROOT.ML +%%DATADIR%%/src/HOL/HahnBanach/Subspace.thy +%%DATADIR%%/src/HOL/HahnBanach/VectorSpace.thy +%%DATADIR%%/src/HOL/HahnBanach/ZornLemma.thy +%%DATADIR%%/src/HOL/HahnBanach/document/root.bib +%%DATADIR%%/src/HOL/HahnBanach/document/root.tex %%DATADIR%%/src/HOL/Hilbert_Choice.thy %%DATADIR%%/src/HOL/Hoare/Arith2.thy %%DATADIR%%/src/HOL/Hoare/Examples.thy @@ -2407,36 +3050,6 @@ %%DATADIR%%/src/HOL/HoareParallel/ROOT.ML %%DATADIR%%/src/HOL/HoareParallel/document/root.bib %%DATADIR%%/src/HOL/HoareParallel/document/root.tex -%%DATADIR%%/src/HOL/Hyperreal/Deriv.thy -%%DATADIR%%/src/HOL/Hyperreal/Fact.thy -%%DATADIR%%/src/HOL/Hyperreal/Filter.thy -%%DATADIR%%/src/HOL/Hyperreal/FrechetDeriv.thy -%%DATADIR%%/src/HOL/Hyperreal/HDeriv.thy -%%DATADIR%%/src/HOL/Hyperreal/HLim.thy -%%DATADIR%%/src/HOL/Hyperreal/HLog.thy -%%DATADIR%%/src/HOL/Hyperreal/HSEQ.thy -%%DATADIR%%/src/HOL/Hyperreal/HSeries.thy -%%DATADIR%%/src/HOL/Hyperreal/HTranscendental.thy -%%DATADIR%%/src/HOL/Hyperreal/HyperDef.thy -%%DATADIR%%/src/HOL/Hyperreal/HyperNat.thy -%%DATADIR%%/src/HOL/Hyperreal/Hyperreal.thy -%%DATADIR%%/src/HOL/Hyperreal/Integration.thy -%%DATADIR%%/src/HOL/Hyperreal/Lim.thy -%%DATADIR%%/src/HOL/Hyperreal/Ln.thy -%%DATADIR%%/src/HOL/Hyperreal/Log.thy -%%DATADIR%%/src/HOL/Hyperreal/MacLaurin.thy -%%DATADIR%%/src/HOL/Hyperreal/NSA.thy -%%DATADIR%%/src/HOL/Hyperreal/NatStar.thy -%%DATADIR%%/src/HOL/Hyperreal/NthRoot.thy -%%DATADIR%%/src/HOL/Hyperreal/Poly.thy -%%DATADIR%%/src/HOL/Hyperreal/SEQ.thy -%%DATADIR%%/src/HOL/Hyperreal/Series.thy -%%DATADIR%%/src/HOL/Hyperreal/Star.thy -%%DATADIR%%/src/HOL/Hyperreal/StarDef.thy -%%DATADIR%%/src/HOL/Hyperreal/Taylor.thy -%%DATADIR%%/src/HOL/Hyperreal/Transcendental.thy -%%DATADIR%%/src/HOL/Hyperreal/hypreal_arith.ML -%%DATADIR%%/src/HOL/Hyperreal/transfer.ML %%DATADIR%%/src/HOL/IMP/Com.thy %%DATADIR%%/src/HOL/IMP/Compiler.thy %%DATADIR%%/src/HOL/IMP/Compiler0.thy @@ -2444,6 +3057,7 @@ %%DATADIR%%/src/HOL/IMP/Examples.thy %%DATADIR%%/src/HOL/IMP/Expr.thy %%DATADIR%%/src/HOL/IMP/Hoare.thy +%%DATADIR%%/src/HOL/IMP/Live.thy %%DATADIR%%/src/HOL/IMP/Machines.thy %%DATADIR%%/src/HOL/IMP/Natural.thy %%DATADIR%%/src/HOL/IMP/ROOT.ML @@ -2463,6 +3077,17 @@ %%DATADIR%%/src/HOL/IOA/README.html %%DATADIR%%/src/HOL/IOA/ROOT.ML %%DATADIR%%/src/HOL/IOA/Solve.thy +%%DATADIR%%/src/HOL/Imperative_HOL/Array.thy +%%DATADIR%%/src/HOL/Imperative_HOL/Heap.thy +%%DATADIR%%/src/HOL/Imperative_HOL/Heap_Monad.thy +%%DATADIR%%/src/HOL/Imperative_HOL/Imperative_HOL.thy +%%DATADIR%%/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy +%%DATADIR%%/src/HOL/Imperative_HOL/ROOT.ML +%%DATADIR%%/src/HOL/Imperative_HOL/Ref.thy +%%DATADIR%%/src/HOL/Imperative_HOL/Relational.thy +%%DATADIR%%/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy +%%DATADIR%%/src/HOL/Imperative_HOL/ex/Subarray.thy +%%DATADIR%%/src/HOL/Imperative_HOL/ex/Sublist.thy %%DATADIR%%/src/HOL/Import/Generate-HOL/GenHOL4Base.thy %%DATADIR%%/src/HOL/Import/Generate-HOL/GenHOL4Prob.thy %%DATADIR%%/src/HOL/Import/Generate-HOL/GenHOL4Real.thy @@ -2557,7 +3182,6 @@ %%DATADIR%%/src/HOL/Induct/Common_Patterns.thy %%DATADIR%%/src/HOL/Induct/LFilter.thy %%DATADIR%%/src/HOL/Induct/LList.thy -%%DATADIR%%/src/HOL/Induct/Mutil.thy %%DATADIR%%/src/HOL/Induct/Ordinals.thy %%DATADIR%%/src/HOL/Induct/PropLog.thy %%DATADIR%%/src/HOL/Induct/QuoDataType.thy @@ -2571,7 +3195,9 @@ %%DATADIR%%/src/HOL/Induct/Tree.thy %%DATADIR%%/src/HOL/Induct/document/root.tex %%DATADIR%%/src/HOL/Inductive.thy +%%DATADIR%%/src/HOL/Int.thy %%DATADIR%%/src/HOL/IntDiv.thy +%%DATADIR%%/src/HOL/Integration.thy %%DATADIR%%/src/HOL/IsaMakefile %%DATADIR%%/src/HOL/Isar_examples/BasicLogic.thy %%DATADIR%%/src/HOL/Isar_examples/Cantor.thy @@ -2622,6 +3248,7 @@ %%DATADIR%%/src/HOL/Library/AssocList.thy %%DATADIR%%/src/HOL/Library/BigO.thy %%DATADIR%%/src/HOL/Library/Binomial.thy +%%DATADIR%%/src/HOL/Library/Bit.thy %%DATADIR%%/src/HOL/Library/Boolean_Algebra.thy %%DATADIR%%/src/HOL/Library/Char_nat.thy %%DATADIR%%/src/HOL/Library/Char_ord.thy @@ -2629,58 +3256,90 @@ %%DATADIR%%/src/HOL/Library/Code_Char_chr.thy %%DATADIR%%/src/HOL/Library/Code_Index.thy %%DATADIR%%/src/HOL/Library/Code_Integer.thy -%%DATADIR%%/src/HOL/Library/Code_Message.thy %%DATADIR%%/src/HOL/Library/Coinductive_List.thy %%DATADIR%%/src/HOL/Library/Commutative_Ring.thy +%%DATADIR%%/src/HOL/Library/ContNotDenum.thy %%DATADIR%%/src/HOL/Library/Continuity.thy +%%DATADIR%%/src/HOL/Library/Countable.thy +%%DATADIR%%/src/HOL/Library/Determinants.thy +%%DATADIR%%/src/HOL/Library/Diagonalize.thy %%DATADIR%%/src/HOL/Library/Efficient_Nat.thy -%%DATADIR%%/src/HOL/Library/Eval.thy +%%DATADIR%%/src/HOL/Library/Enum.thy +%%DATADIR%%/src/HOL/Library/Euclidean_Space.thy %%DATADIR%%/src/HOL/Library/Eval_Witness.thy %%DATADIR%%/src/HOL/Library/Executable_Set.thy +%%DATADIR%%/src/HOL/Library/Finite_Cartesian_Product.thy +%%DATADIR%%/src/HOL/Library/Float.thy +%%DATADIR%%/src/HOL/Library/Formal_Power_Series.thy +%%DATADIR%%/src/HOL/Library/FrechetDeriv.thy %%DATADIR%%/src/HOL/Library/FuncSet.thy -%%DATADIR%%/src/HOL/Library/GCD.thy +%%DATADIR%%/src/HOL/Library/Fundamental_Theorem_Algebra.thy +%%DATADIR%%/src/HOL/Library/Glbs.thy %%DATADIR%%/src/HOL/Library/Infinite_Set.thy +%%DATADIR%%/src/HOL/Library/Inner_Product.thy %%DATADIR%%/src/HOL/Library/LaTeXsugar.thy +%%DATADIR%%/src/HOL/Library/Lattice_Syntax.thy %%DATADIR%%/src/HOL/Library/Library.thy %%DATADIR%%/src/HOL/Library/Library/ROOT.ML %%DATADIR%%/src/HOL/Library/Library/document/root.bib %%DATADIR%%/src/HOL/Library/Library/document/root.tex +%%DATADIR%%/src/HOL/Library/ListVector.thy %%DATADIR%%/src/HOL/Library/List_Prefix.thy %%DATADIR%%/src/HOL/Library/List_lexord.thy +%%DATADIR%%/src/HOL/Library/Mapping.thy %%DATADIR%%/src/HOL/Library/Multiset.thy -%%DATADIR%%/src/HOL/Library/NatPair.thy %%DATADIR%%/src/HOL/Library/Nat_Infinity.thy +%%DATADIR%%/src/HOL/Library/Nat_Int_Bij.thy %%DATADIR%%/src/HOL/Library/Nested_Environment.thy %%DATADIR%%/src/HOL/Library/Numeral_Type.thy +%%DATADIR%%/src/HOL/Library/Option_ord.thy %%DATADIR%%/src/HOL/Library/OptionalSugar.thy -%%DATADIR%%/src/HOL/Library/Parity.thy +%%DATADIR%%/src/HOL/Library/Order_Relation.thy %%DATADIR%%/src/HOL/Library/Permutation.thy +%%DATADIR%%/src/HOL/Library/Permutations.thy +%%DATADIR%%/src/HOL/Library/Pocklington.thy +%%DATADIR%%/src/HOL/Library/Poly_Deriv.thy +%%DATADIR%%/src/HOL/Library/Polynomial.thy %%DATADIR%%/src/HOL/Library/Primes.thy +%%DATADIR%%/src/HOL/Library/Product_Vector.thy %%DATADIR%%/src/HOL/Library/Product_ord.thy +%%DATADIR%%/src/HOL/Library/Product_plus.thy +%%DATADIR%%/src/HOL/Library/Quickcheck.thy %%DATADIR%%/src/HOL/Library/Quicksort.thy %%DATADIR%%/src/HOL/Library/Quotient.thy +%%DATADIR%%/src/HOL/Library/RBT.thy %%DATADIR%%/src/HOL/Library/README.html %%DATADIR%%/src/HOL/Library/Ramsey.thy +%%DATADIR%%/src/HOL/Library/Random.thy +%%DATADIR%%/src/HOL/Library/Reflection.thy %%DATADIR%%/src/HOL/Library/SetsAndFunctions.thy %%DATADIR%%/src/HOL/Library/State_Monad.thy +%%DATADIR%%/src/HOL/Library/Sublist_Order.thy +%%DATADIR%%/src/HOL/Library/Topology_Euclidean_Space.thy +%%DATADIR%%/src/HOL/Library/Univ_Poly.thy %%DATADIR%%/src/HOL/Library/While_Combinator.thy %%DATADIR%%/src/HOL/Library/Word.thy %%DATADIR%%/src/HOL/Library/Zorn.thy %%DATADIR%%/src/HOL/Library/comm_ring.ML +%%DATADIR%%/src/HOL/Library/normarith.ML +%%DATADIR%%/src/HOL/Library/reflection.ML +%%DATADIR%%/src/HOL/Library/reify_data.ML +%%DATADIR%%/src/HOL/Lim.thy %%DATADIR%%/src/HOL/List.thy +%%DATADIR%%/src/HOL/Ln.thy +%%DATADIR%%/src/HOL/Log.thy +%%DATADIR%%/src/HOL/Lubs.thy +%%DATADIR%%/src/HOL/MacLaurin.thy %%DATADIR%%/src/HOL/Main.thy %%DATADIR%%/src/HOL/Map.thy %%DATADIR%%/src/HOL/Matrix/LP.thy %%DATADIR%%/src/HOL/Matrix/Matrix.thy -%%DATADIR%%/src/HOL/Matrix/MatrixGeneral.thy %%DATADIR%%/src/HOL/Matrix/ROOT.ML %%DATADIR%%/src/HOL/Matrix/SparseMatrix.thy %%DATADIR%%/src/HOL/Matrix/cplex/Cplex.thy %%DATADIR%%/src/HOL/Matrix/cplex/CplexMatrixConverter.ML %%DATADIR%%/src/HOL/Matrix/cplex/Cplex_tools.ML -%%DATADIR%%/src/HOL/Matrix/cplex/FloatSparseMatrix.thy %%DATADIR%%/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML -%%DATADIR%%/src/HOL/Matrix/cplex/MatrixLP.thy %%DATADIR%%/src/HOL/Matrix/cplex/fspmlp.ML %%DATADIR%%/src/HOL/Matrix/cplex/matrixlp.ML %%DATADIR%%/src/HOL/Matrix/document/root.tex @@ -2750,6 +3409,7 @@ %%DATADIR%%/src/HOL/MicroJava/JVM/JVMInstructions.thy %%DATADIR%%/src/HOL/MicroJava/JVM/JVMListExample.thy %%DATADIR%%/src/HOL/MicroJava/JVM/JVMState.thy +%%DATADIR%%/src/HOL/MicroJava/MicroJava.thy %%DATADIR%%/src/HOL/MicroJava/ROOT.ML %%DATADIR%%/src/HOL/MicroJava/document/introduction.tex %%DATADIR%%/src/HOL/MicroJava/document/root.bib @@ -2764,6 +3424,31 @@ %%DATADIR%%/src/HOL/Modelcheck/README.html %%DATADIR%%/src/HOL/Modelcheck/ROOT.ML %%DATADIR%%/src/HOL/Modelcheck/mucke_oracle.ML +%%DATADIR%%/src/HOL/NSA/CLim.thy +%%DATADIR%%/src/HOL/NSA/CStar.thy +%%DATADIR%%/src/HOL/NSA/Examples/NSPrimes.thy +%%DATADIR%%/src/HOL/NSA/Examples/ROOT.ML +%%DATADIR%%/src/HOL/NSA/Filter.thy +%%DATADIR%%/src/HOL/NSA/HDeriv.thy +%%DATADIR%%/src/HOL/NSA/HLim.thy +%%DATADIR%%/src/HOL/NSA/HLog.thy +%%DATADIR%%/src/HOL/NSA/HSEQ.thy +%%DATADIR%%/src/HOL/NSA/HSeries.thy +%%DATADIR%%/src/HOL/NSA/HTranscendental.thy +%%DATADIR%%/src/HOL/NSA/HyperDef.thy +%%DATADIR%%/src/HOL/NSA/HyperNat.thy +%%DATADIR%%/src/HOL/NSA/Hypercomplex.thy +%%DATADIR%%/src/HOL/NSA/Hyperreal.thy +%%DATADIR%%/src/HOL/NSA/NSA.thy +%%DATADIR%%/src/HOL/NSA/NSCA.thy +%%DATADIR%%/src/HOL/NSA/NSComplex.thy +%%DATADIR%%/src/HOL/NSA/NatStar.thy +%%DATADIR%%/src/HOL/NSA/ROOT.ML +%%DATADIR%%/src/HOL/NSA/Star.thy +%%DATADIR%%/src/HOL/NSA/StarDef.thy +%%DATADIR%%/src/HOL/NSA/document/root.tex +%%DATADIR%%/src/HOL/NSA/hypreal_arith.ML +%%DATADIR%%/src/HOL/NSA/transfer.ML %%DATADIR%%/src/HOL/NanoJava/AxSem.thy %%DATADIR%%/src/HOL/NanoJava/Decl.thy %%DATADIR%%/src/HOL/NanoJava/Equivalence.thy @@ -2777,10 +3462,12 @@ %%DATADIR%%/src/HOL/NanoJava/document/root.tex %%DATADIR%%/src/HOL/Nat.thy %%DATADIR%%/src/HOL/NatBin.thy +%%DATADIR%%/src/HOL/Nominal/Examples/CK_Machine.thy %%DATADIR%%/src/HOL/Nominal/Examples/CR.thy %%DATADIR%%/src/HOL/Nominal/Examples/CR_Takahashi.thy %%DATADIR%%/src/HOL/Nominal/Examples/Class.thy %%DATADIR%%/src/HOL/Nominal/Examples/Compile.thy +%%DATADIR%%/src/HOL/Nominal/Examples/Contexts.thy %%DATADIR%%/src/HOL/Nominal/Examples/Crary.thy %%DATADIR%%/src/HOL/Nominal/Examples/Fsub.thy %%DATADIR%%/src/HOL/Nominal/Examples/Height.thy @@ -2790,7 +3477,11 @@ %%DATADIR%%/src/HOL/Nominal/Examples/ROOT.ML %%DATADIR%%/src/HOL/Nominal/Examples/SN.thy %%DATADIR%%/src/HOL/Nominal/Examples/SOS.thy +%%DATADIR%%/src/HOL/Nominal/Examples/Standardization.thy %%DATADIR%%/src/HOL/Nominal/Examples/Support.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/Nominal/Examples/Weakening.thy %%DATADIR%%/src/HOL/Nominal/INSTALL %%DATADIR%%/src/HOL/Nominal/Nominal.thy @@ -2799,10 +3490,12 @@ %%DATADIR%%/src/HOL/Nominal/nominal_fresh_fun.ML %%DATADIR%%/src/HOL/Nominal/nominal_induct.ML %%DATADIR%%/src/HOL/Nominal/nominal_inductive.ML +%%DATADIR%%/src/HOL/Nominal/nominal_inductive2.ML %%DATADIR%%/src/HOL/Nominal/nominal_package.ML %%DATADIR%%/src/HOL/Nominal/nominal_permeq.ML %%DATADIR%%/src/HOL/Nominal/nominal_primrec.ML %%DATADIR%%/src/HOL/Nominal/nominal_thmdecls.ML +%%DATADIR%%/src/HOL/NthRoot.thy %%DATADIR%%/src/HOL/NumberTheory/BijectionRel.thy %%DATADIR%%/src/HOL/NumberTheory/Chinese.thy %%DATADIR%%/src/HOL/NumberTheory/Euler.thy @@ -2821,8 +3514,12 @@ %%DATADIR%%/src/HOL/NumberTheory/WilsonBij.thy %%DATADIR%%/src/HOL/NumberTheory/WilsonRuss.thy %%DATADIR%%/src/HOL/NumberTheory/document/root.tex +%%DATADIR%%/src/HOL/Option.thy %%DATADIR%%/src/HOL/OrderedGroup.thy %%DATADIR%%/src/HOL/Orderings.thy +%%DATADIR%%/src/HOL/PReal.thy +%%DATADIR%%/src/HOL/Parity.thy +%%DATADIR%%/src/HOL/Plain.thy %%DATADIR%%/src/HOL/Power.thy %%DATADIR%%/src/HOL/Predicate.thy %%DATADIR%%/src/HOL/Presburger.thy @@ -2834,37 +3531,14 @@ %%DATADIR%%/src/HOL/Prolog/Test.thy %%DATADIR%%/src/HOL/Prolog/Type.thy %%DATADIR%%/src/HOL/Prolog/prolog.ML +%%DATADIR%%/src/HOL/RComplete.thy %%DATADIR%%/src/HOL/README.html %%DATADIR%%/src/HOL/ROOT.ML -%%DATADIR%%/src/HOL/Real/ContNotDenum.thy -%%DATADIR%%/src/HOL/Real/Float.thy -%%DATADIR%%/src/HOL/Real/HahnBanach/Bounds.thy -%%DATADIR%%/src/HOL/Real/HahnBanach/FunctionNorm.thy -%%DATADIR%%/src/HOL/Real/HahnBanach/FunctionOrder.thy -%%DATADIR%%/src/HOL/Real/HahnBanach/HahnBanach.thy -%%DATADIR%%/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy -%%DATADIR%%/src/HOL/Real/HahnBanach/HahnBanachLemmas.thy -%%DATADIR%%/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy -%%DATADIR%%/src/HOL/Real/HahnBanach/Linearform.thy -%%DATADIR%%/src/HOL/Real/HahnBanach/NormedSpace.thy -%%DATADIR%%/src/HOL/Real/HahnBanach/README.html -%%DATADIR%%/src/HOL/Real/HahnBanach/ROOT.ML -%%DATADIR%%/src/HOL/Real/HahnBanach/Subspace.thy -%%DATADIR%%/src/HOL/Real/HahnBanach/VectorSpace.thy -%%DATADIR%%/src/HOL/Real/HahnBanach/ZornLemma.thy -%%DATADIR%%/src/HOL/Real/HahnBanach/document/root.bib -%%DATADIR%%/src/HOL/Real/HahnBanach/document/root.tex -%%DATADIR%%/src/HOL/Real/Lubs.thy -%%DATADIR%%/src/HOL/Real/PReal.thy -%%DATADIR%%/src/HOL/Real/RComplete.thy -%%DATADIR%%/src/HOL/Real/Rational.thy -%%DATADIR%%/src/HOL/Real/Real.thy -%%DATADIR%%/src/HOL/Real/RealDef.thy -%%DATADIR%%/src/HOL/Real/RealPow.thy -%%DATADIR%%/src/HOL/Real/RealVector.thy -%%DATADIR%%/src/HOL/Real/float_arith.ML -%%DATADIR%%/src/HOL/Real/rat_arith.ML -%%DATADIR%%/src/HOL/Real/real_arith.ML +%%DATADIR%%/src/HOL/Rational.thy +%%DATADIR%%/src/HOL/Real.thy +%%DATADIR%%/src/HOL/RealDef.thy +%%DATADIR%%/src/HOL/RealPow.thy +%%DATADIR%%/src/HOL/RealVector.thy %%DATADIR%%/src/HOL/Recdef.thy %%DATADIR%%/src/HOL/Record.thy %%DATADIR%%/src/HOL/Refute.thy @@ -2872,6 +3546,7 @@ %%DATADIR%%/src/HOL/Relation_Power.thy %%DATADIR%%/src/HOL/Ring_and_Field.thy %%DATADIR%%/src/HOL/SAT.thy +%%DATADIR%%/src/HOL/SEQ.thy %%DATADIR%%/src/HOL/SET-Protocol/Cardholder_Registration.thy %%DATADIR%%/src/HOL/SET-Protocol/EventSET.thy %%DATADIR%%/src/HOL/SET-Protocol/Merchant_Registration.thy @@ -2880,6 +3555,7 @@ %%DATADIR%%/src/HOL/SET-Protocol/Purchase.thy %%DATADIR%%/src/HOL/SET-Protocol/ROOT.ML %%DATADIR%%/src/HOL/SET-Protocol/document/root.tex +%%DATADIR%%/src/HOL/Series.thy %%DATADIR%%/src/HOL/Set.thy %%DATADIR%%/src/HOL/SetInterval.thy %%DATADIR%%/src/HOL/SizeChange/Correctness.thy @@ -2933,6 +3609,8 @@ %%DATADIR%%/src/HOL/TLA/ROOT.ML %%DATADIR%%/src/HOL/TLA/Stfun.thy %%DATADIR%%/src/HOL/TLA/TLA.thy +%%DATADIR%%/src/HOL/Taylor.thy +%%DATADIR%%/src/HOL/Tools/ComputeFloat.thy %%DATADIR%%/src/HOL/Tools/ComputeHOL.thy %%DATADIR%%/src/HOL/Tools/ComputeNumeral.thy %%DATADIR%%/src/HOL/Tools/Groebner_Basis/groebner.ML @@ -2957,6 +3635,9 @@ %%DATADIR%%/src/HOL/Tools/TFL/thry.ML %%DATADIR%%/src/HOL/Tools/TFL/usyntax.ML %%DATADIR%%/src/HOL/Tools/TFL/utils.ML +%%DATADIR%%/src/HOL/Tools/arith_data.ML +%%DATADIR%%/src/HOL/Tools/atp_manager.ML +%%DATADIR%%/src/HOL/Tools/atp_wrapper.ML %%DATADIR%%/src/HOL/Tools/cnf_funcs.ML %%DATADIR%%/src/HOL/Tools/datatype_abs_proofs.ML %%DATADIR%%/src/HOL/Tools/datatype_aux.ML @@ -2967,38 +3648,54 @@ %%DATADIR%%/src/HOL/Tools/datatype_realizer.ML %%DATADIR%%/src/HOL/Tools/datatype_rep_proofs.ML %%DATADIR%%/src/HOL/Tools/dseq.ML +%%DATADIR%%/src/HOL/Tools/float_arith.ML +%%DATADIR%%/src/HOL/Tools/float_syntax.ML %%DATADIR%%/src/HOL/Tools/function_package/auto_term.ML %%DATADIR%%/src/HOL/Tools/function_package/context_tree.ML +%%DATADIR%%/src/HOL/Tools/function_package/decompose.ML +%%DATADIR%%/src/HOL/Tools/function_package/descent.ML %%DATADIR%%/src/HOL/Tools/function_package/fundef_common.ML %%DATADIR%%/src/HOL/Tools/function_package/fundef_core.ML %%DATADIR%%/src/HOL/Tools/function_package/fundef_datatype.ML %%DATADIR%%/src/HOL/Tools/function_package/fundef_lib.ML %%DATADIR%%/src/HOL/Tools/function_package/fundef_package.ML +%%DATADIR%%/src/HOL/Tools/function_package/induction_scheme.ML %%DATADIR%%/src/HOL/Tools/function_package/inductive_wrap.ML %%DATADIR%%/src/HOL/Tools/function_package/lexicographic_order.ML +%%DATADIR%%/src/HOL/Tools/function_package/measure_functions.ML %%DATADIR%%/src/HOL/Tools/function_package/mutual.ML %%DATADIR%%/src/HOL/Tools/function_package/pattern_split.ML +%%DATADIR%%/src/HOL/Tools/function_package/scnp_reconstruct.ML +%%DATADIR%%/src/HOL/Tools/function_package/scnp_solve.ML %%DATADIR%%/src/HOL/Tools/function_package/size.ML +%%DATADIR%%/src/HOL/Tools/function_package/sum_tree.ML +%%DATADIR%%/src/HOL/Tools/function_package/termination.ML +%%DATADIR%%/src/HOL/Tools/hologic.ML %%DATADIR%%/src/HOL/Tools/inductive_codegen.ML %%DATADIR%%/src/HOL/Tools/inductive_package.ML %%DATADIR%%/src/HOL/Tools/inductive_realizer.ML %%DATADIR%%/src/HOL/Tools/inductive_set_package.ML +%%DATADIR%%/src/HOL/Tools/int_arith.ML +%%DATADIR%%/src/HOL/Tools/int_factor_simprocs.ML %%DATADIR%%/src/HOL/Tools/lin_arith.ML %%DATADIR%%/src/HOL/Tools/meson.ML %%DATADIR%%/src/HOL/Tools/metis_tools.ML +%%DATADIR%%/src/HOL/Tools/nat_arith.ML +%%DATADIR%%/src/HOL/Tools/nat_simprocs.ML %%DATADIR%%/src/HOL/Tools/numeral.ML %%DATADIR%%/src/HOL/Tools/numeral_syntax.ML +%%DATADIR%%/src/HOL/Tools/old_primrec_package.ML %%DATADIR%%/src/HOL/Tools/polyhash.ML %%DATADIR%%/src/HOL/Tools/primrec_package.ML %%DATADIR%%/src/HOL/Tools/prop_logic.ML +%%DATADIR%%/src/HOL/Tools/rat_arith.ML +%%DATADIR%%/src/HOL/Tools/real_arith.ML %%DATADIR%%/src/HOL/Tools/recdef_package.ML %%DATADIR%%/src/HOL/Tools/recfun_codegen.ML %%DATADIR%%/src/HOL/Tools/record_package.ML %%DATADIR%%/src/HOL/Tools/refute.ML %%DATADIR%%/src/HOL/Tools/refute_isar.ML %%DATADIR%%/src/HOL/Tools/res_atp.ML -%%DATADIR%%/src/HOL/Tools/res_atp_methods.ML -%%DATADIR%%/src/HOL/Tools/res_atp_provers.ML %%DATADIR%%/src/HOL/Tools/res_axioms.ML %%DATADIR%%/src/HOL/Tools/res_clause.ML %%DATADIR%%/src/HOL/Tools/res_hol_clause.ML @@ -3006,15 +3703,17 @@ %%DATADIR%%/src/HOL/Tools/rewrite_hol_proof.ML %%DATADIR%%/src/HOL/Tools/sat_funcs.ML %%DATADIR%%/src/HOL/Tools/sat_solver.ML +%%DATADIR%%/src/HOL/Tools/simpdata.ML %%DATADIR%%/src/HOL/Tools/specification_package.ML %%DATADIR%%/src/HOL/Tools/split_rule.ML %%DATADIR%%/src/HOL/Tools/string_syntax.ML %%DATADIR%%/src/HOL/Tools/typecopy_package.ML %%DATADIR%%/src/HOL/Tools/typedef_codegen.ML %%DATADIR%%/src/HOL/Tools/typedef_package.ML -%%DATADIR%%/src/HOL/Tools/watcher.ML +%%DATADIR%%/src/HOL/Transcendental.thy %%DATADIR%%/src/HOL/Transitive_Closure.thy %%DATADIR%%/src/HOL/Typedef.thy +%%DATADIR%%/src/HOL/Typerep.thy %%DATADIR%%/src/HOL/UNITY/Comp.thy %%DATADIR%%/src/HOL/UNITY/Comp/Alloc.thy %%DATADIR%%/src/HOL/UNITY/Comp/AllocBase.thy @@ -3070,6 +3769,7 @@ %%DATADIR%%/src/HOL/W0/ROOT.ML %%DATADIR%%/src/HOL/W0/W0.thy %%DATADIR%%/src/HOL/W0/document/root.tex +%%DATADIR%%/src/HOL/Wellfounded.thy %%DATADIR%%/src/HOL/Word/BinBoolList.thy %%DATADIR%%/src/HOL/Word/BinGeneral.thy %%DATADIR%%/src/HOL/Word/BinOperations.thy @@ -3080,11 +3780,11 @@ %%DATADIR%%/src/HOL/Word/ROOT.ML %%DATADIR%%/src/HOL/Word/Size.thy %%DATADIR%%/src/HOL/Word/TdThs.thy +%%DATADIR%%/src/HOL/Word/Word.thy %%DATADIR%%/src/HOL/Word/WordArith.thy %%DATADIR%%/src/HOL/Word/WordBitwise.thy %%DATADIR%%/src/HOL/Word/WordDefinition.thy %%DATADIR%%/src/HOL/Word/WordGenLib.thy -%%DATADIR%%/src/HOL/Word/WordMain.thy %%DATADIR%%/src/HOL/Word/WordShift.thy %%DATADIR%%/src/HOL/Word/document/root.bib %%DATADIR%%/src/HOL/Word/document/root.tex @@ -3096,40 +3796,44 @@ %%DATADIR%%/src/HOL/ZF/ROOT.ML %%DATADIR%%/src/HOL/ZF/Zet.thy %%DATADIR%%/src/HOL/ZF/document/root.tex -%%DATADIR%%/src/HOL/arith_data.ML +%%DATADIR%%/src/HOL/base.ML %%DATADIR%%/src/HOL/document/root.bib %%DATADIR%%/src/HOL/document/root.tex %%DATADIR%%/src/HOL/ex/Abstract_NAT.thy %%DATADIR%%/src/HOL/ex/Adder.thy %%DATADIR%%/src/HOL/ex/Antiquote.thy %%DATADIR%%/src/HOL/ex/Arith_Examples.thy +%%DATADIR%%/src/HOL/ex/Arithmetic_Series_Complex.thy %%DATADIR%%/src/HOL/ex/BT.thy %%DATADIR%%/src/HOL/ex/BinEx.thy %%DATADIR%%/src/HOL/ex/Binary.thy %%DATADIR%%/src/HOL/ex/CTL.thy %%DATADIR%%/src/HOL/ex/Chinese.thy %%DATADIR%%/src/HOL/ex/Classical.thy +%%DATADIR%%/src/HOL/ex/CodegenSML_Test.thy %%DATADIR%%/src/HOL/ex/Codegenerator.thy %%DATADIR%%/src/HOL/ex/Codegenerator_Pretty.thy +%%DATADIR%%/src/HOL/ex/Coherent.thy %%DATADIR%%/src/HOL/ex/Commutative_RingEx.thy %%DATADIR%%/src/HOL/ex/Commutative_Ring_Complete.thy -%%DATADIR%%/src/HOL/ex/Dense_Linear_Order_Ex.thy +%%DATADIR%%/src/HOL/ex/Efficient_Nat_examples.thy %%DATADIR%%/src/HOL/ex/Eval_Examples.thy %%DATADIR%%/src/HOL/ex/ExecutableContent.thy +%%DATADIR%%/src/HOL/ex/Formal_Power_Series_Examples.thy %%DATADIR%%/src/HOL/ex/Fundefs.thy %%DATADIR%%/src/HOL/ex/Groebner_Examples.thy %%DATADIR%%/src/HOL/ex/Guess.thy +%%DATADIR%%/src/HOL/ex/HarmonicSeries.thy %%DATADIR%%/src/HOL/ex/Hebrew.thy %%DATADIR%%/src/HOL/ex/Hex_Bin_Examples.thy %%DATADIR%%/src/HOL/ex/Higher_Order_Logic.thy %%DATADIR%%/src/HOL/ex/Hilbert_Classical.thy +%%DATADIR%%/src/HOL/ex/Induction_Scheme.thy %%DATADIR%%/src/HOL/ex/InductiveInvariant.thy %%DATADIR%%/src/HOL/ex/InductiveInvariant_examples.thy %%DATADIR%%/src/HOL/ex/Intuitionistic.thy %%DATADIR%%/src/HOL/ex/Lagrange.thy -%%DATADIR%%/src/HOL/ex/LexOrds.thy %%DATADIR%%/src/HOL/ex/LocaleTest2.thy -%%DATADIR%%/src/HOL/ex/Locales.thy %%DATADIR%%/src/HOL/ex/MT.thy %%DATADIR%%/src/HOL/ex/MergeSort.thy %%DATADIR%%/src/HOL/ex/Meson_Test.thy @@ -3137,47 +3841,52 @@ %%DATADIR%%/src/HOL/ex/Multiquote.thy %%DATADIR%%/src/HOL/ex/NatSum.thy %%DATADIR%%/src/HOL/ex/NormalForm.thy +%%DATADIR%%/src/HOL/ex/Numeral.thy %%DATADIR%%/src/HOL/ex/PER.thy +%%DATADIR%%/src/HOL/ex/Predicate_Compile.thy %%DATADIR%%/src/HOL/ex/PresburgerEx.thy %%DATADIR%%/src/HOL/ex/Primrec.thy -%%DATADIR%%/src/HOL/ex/Puzzle.thy %%DATADIR%%/src/HOL/ex/Quickcheck_Examples.thy +%%DATADIR%%/src/HOL/ex/Quickcheck_Generators.thy %%DATADIR%%/src/HOL/ex/README.html %%DATADIR%%/src/HOL/ex/ROOT.ML -%%DATADIR%%/src/HOL/ex/Random.thy %%DATADIR%%/src/HOL/ex/Recdefs.thy %%DATADIR%%/src/HOL/ex/Records.thy -%%DATADIR%%/src/HOL/ex/Reflected_Presburger.thy -%%DATADIR%%/src/HOL/ex/Reflection.thy %%DATADIR%%/src/HOL/ex/ReflectionEx.thy %%DATADIR%%/src/HOL/ex/Refute_Examples.thy %%DATADIR%%/src/HOL/ex/SAT_Examples.thy %%DATADIR%%/src/HOL/ex/SVC_Oracle.thy +%%DATADIR%%/src/HOL/ex/Serbian.thy %%DATADIR%%/src/HOL/ex/Sorting.thy +%%DATADIR%%/src/HOL/ex/Sqrt.thy +%%DATADIR%%/src/HOL/ex/Sqrt_Script.thy %%DATADIR%%/src/HOL/ex/Sudoku.thy %%DATADIR%%/src/HOL/ex/Tarski.thy +%%DATADIR%%/src/HOL/ex/Term_Of_Syntax.thy +%%DATADIR%%/src/HOL/ex/Termination.thy %%DATADIR%%/src/HOL/ex/ThreeDivides.thy %%DATADIR%%/src/HOL/ex/Unification.thy -%%DATADIR%%/src/HOL/ex/coopereif.ML -%%DATADIR%%/src/HOL/ex/coopertac.ML %%DATADIR%%/src/HOL/ex/document/root.bib %%DATADIR%%/src/HOL/ex/document/root.tex -%%DATADIR%%/src/HOL/ex/reflection.ML -%%DATADIR%%/src/HOL/ex/reflection_data.ML +%%DATADIR%%/src/HOL/ex/predicate_compile.ML %%DATADIR%%/src/HOL/ex/set.thy %%DATADIR%%/src/HOL/ex/svc_funcs.ML %%DATADIR%%/src/HOL/ex/svc_test.thy -%%DATADIR%%/src/HOL/hologic.ML -%%DATADIR%%/src/HOL/int_arith1.ML -%%DATADIR%%/src/HOL/int_factor_simprocs.ML -%%DATADIR%%/src/HOL/nat_simprocs.ML -%%DATADIR%%/src/HOL/simpdata.ML +%%DATADIR%%/src/HOL/main.ML +%%DATADIR%%/src/HOL/plain.ML %%DATADIR%%/src/HOLCF/Adm.thy +%%DATADIR%%/src/HOLCF/Algebraic.thy +%%DATADIR%%/src/HOLCF/Bifinite.thy %%DATADIR%%/src/HOLCF/Cfun.thy +%%DATADIR%%/src/HOLCF/CompactBasis.thy +%%DATADIR%%/src/HOLCF/Completion.thy %%DATADIR%%/src/HOLCF/Cont.thy +%%DATADIR%%/src/HOLCF/ConvexPD.thy %%DATADIR%%/src/HOLCF/Cprod.thy +%%DATADIR%%/src/HOLCF/Deflation.thy %%DATADIR%%/src/HOLCF/Discrete.thy %%DATADIR%%/src/HOLCF/Domain.thy +%%DATADIR%%/src/HOLCF/Eventual.thy %%DATADIR%%/src/HOLCF/FOCUS/Buffer.thy %%DATADIR%%/src/HOLCF/FOCUS/Buffer_adm.thy %%DATADIR%%/src/HOLCF/FOCUS/FOCUS.thy @@ -3190,12 +3899,6 @@ %%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 @@ -3268,14 +3971,18 @@ %%DATADIR%%/src/HOLCF/IOA/meta_theory/ioa_package.ML %%DATADIR%%/src/HOLCF/IsaMakefile %%DATADIR%%/src/HOLCF/Lift.thy +%%DATADIR%%/src/HOLCF/LowerPD.thy +%%DATADIR%%/src/HOLCF/NatIso.thy %%DATADIR%%/src/HOLCF/One.thy %%DATADIR%%/src/HOLCF/Pcpo.thy %%DATADIR%%/src/HOLCF/Pcpodef.thy %%DATADIR%%/src/HOLCF/Porder.thy +%%DATADIR%%/src/HOLCF/Product_Cpo.thy %%DATADIR%%/src/HOLCF/README.html %%DATADIR%%/src/HOLCF/ROOT.ML %%DATADIR%%/src/HOLCF/Sprod.thy %%DATADIR%%/src/HOLCF/Ssum.thy +%%DATADIR%%/src/HOLCF/Sum_Cpo.thy %%DATADIR%%/src/HOLCF/Tools/adm_tac.ML %%DATADIR%%/src/HOLCF/Tools/cont_consts.ML %%DATADIR%%/src/HOLCF/Tools/cont_proc.ML @@ -3287,7 +3994,9 @@ %%DATADIR%%/src/HOLCF/Tools/fixrec_package.ML %%DATADIR%%/src/HOLCF/Tools/pcpodef_package.ML %%DATADIR%%/src/HOLCF/Tr.thy +%%DATADIR%%/src/HOLCF/Universal.thy %%DATADIR%%/src/HOLCF/Up.thy +%%DATADIR%%/src/HOLCF/UpperPD.thy %%DATADIR%%/src/HOLCF/document/root.tex %%DATADIR%%/src/HOLCF/ex/Dagstuhl.thy %%DATADIR%%/src/HOLCF/ex/Dnat.thy @@ -3296,6 +4005,7 @@ %%DATADIR%%/src/HOLCF/ex/Focus_ex.thy %%DATADIR%%/src/HOLCF/ex/Hoare.thy %%DATADIR%%/src/HOLCF/ex/Loop.thy +%%DATADIR%%/src/HOLCF/ex/Powerdomain_ex.thy %%DATADIR%%/src/HOLCF/ex/ROOT.ML %%DATADIR%%/src/HOLCF/ex/Stream.thy %%DATADIR%%/src/HOLCF/ex/hoare.txt @@ -3323,104 +4033,141 @@ %%DATADIR%%/src/Provers/blast.ML %%DATADIR%%/src/Provers/clasimp.ML %%DATADIR%%/src/Provers/classical.ML -%%DATADIR%%/src/Provers/eqsubst.ML %%DATADIR%%/src/Provers/hypsubst.ML %%DATADIR%%/src/Provers/order.ML -%%DATADIR%%/src/Provers/project_rule.ML %%DATADIR%%/src/Provers/quantifier1.ML %%DATADIR%%/src/Provers/quasi.ML %%DATADIR%%/src/Provers/splitter.ML %%DATADIR%%/src/Provers/trancl.ML %%DATADIR%%/src/Provers/typedsimp.ML +%%DATADIR%%/src/Pure/Concurrent/ROOT.ML +%%DATADIR%%/src/Pure/Concurrent/future.ML +%%DATADIR%%/src/Pure/Concurrent/mailbox.ML +%%DATADIR%%/src/Pure/Concurrent/par_list.ML +%%DATADIR%%/src/Pure/Concurrent/par_list_dummy.ML +%%DATADIR%%/src/Pure/Concurrent/simple_thread.ML +%%DATADIR%%/src/Pure/Concurrent/synchronized.ML +%%DATADIR%%/src/Pure/Concurrent/task_queue.ML %%DATADIR%%/src/Pure/General/ROOT.ML %%DATADIR%%/src/Pure/General/alist.ML +%%DATADIR%%/src/Pure/General/antiquote.ML %%DATADIR%%/src/Pure/General/balanced_tree.ML %%DATADIR%%/src/Pure/General/basics.ML +%%DATADIR%%/src/Pure/General/binding.ML %%DATADIR%%/src/Pure/General/buffer.ML +%%DATADIR%%/src/Pure/General/event_bus.scala %%DATADIR%%/src/Pure/General/file.ML %%DATADIR%%/src/Pure/General/graph.ML %%DATADIR%%/src/Pure/General/heap.ML -%%DATADIR%%/src/Pure/General/history.ML %%DATADIR%%/src/Pure/General/integer.ML +%%DATADIR%%/src/Pure/General/lazy.ML +%%DATADIR%%/src/Pure/General/long_name.ML %%DATADIR%%/src/Pure/General/markup.ML +%%DATADIR%%/src/Pure/General/markup.scala %%DATADIR%%/src/Pure/General/name_space.ML %%DATADIR%%/src/Pure/General/ord_list.ML %%DATADIR%%/src/Pure/General/output.ML %%DATADIR%%/src/Pure/General/path.ML %%DATADIR%%/src/Pure/General/position.ML +%%DATADIR%%/src/Pure/General/position.scala %%DATADIR%%/src/Pure/General/pretty.ML %%DATADIR%%/src/Pure/General/print_mode.ML +%%DATADIR%%/src/Pure/General/properties.ML +%%DATADIR%%/src/Pure/General/queue.ML %%DATADIR%%/src/Pure/General/scan.ML %%DATADIR%%/src/Pure/General/secure.ML %%DATADIR%%/src/Pure/General/seq.ML %%DATADIR%%/src/Pure/General/source.ML %%DATADIR%%/src/Pure/General/stack.ML -%%DATADIR%%/src/Pure/General/susp.ML +%%DATADIR%%/src/Pure/General/swing.scala %%DATADIR%%/src/Pure/General/symbol.ML +%%DATADIR%%/src/Pure/General/symbol.scala +%%DATADIR%%/src/Pure/General/symbol_pos.ML %%DATADIR%%/src/Pure/General/table.ML %%DATADIR%%/src/Pure/General/url.ML %%DATADIR%%/src/Pure/General/xml.ML +%%DATADIR%%/src/Pure/General/xml.scala +%%DATADIR%%/src/Pure/General/yxml.ML +%%DATADIR%%/src/Pure/General/yxml.scala %%DATADIR%%/src/Pure/IsaMakefile %%DATADIR%%/src/Pure/Isar/ROOT.ML -%%DATADIR%%/src/Pure/Isar/antiquote.ML %%DATADIR%%/src/Pure/Isar/args.ML %%DATADIR%%/src/Pure/Isar/attrib.ML %%DATADIR%%/src/Pure/Isar/auto_bind.ML %%DATADIR%%/src/Pure/Isar/calculation.ML %%DATADIR%%/src/Pure/Isar/class.ML +%%DATADIR%%/src/Pure/Isar/class_target.ML %%DATADIR%%/src/Pure/Isar/code.ML %%DATADIR%%/src/Pure/Isar/code_unit.ML %%DATADIR%%/src/Pure/Isar/constdefs.ML %%DATADIR%%/src/Pure/Isar/context_rules.ML %%DATADIR%%/src/Pure/Isar/element.ML -%%DATADIR%%/src/Pure/Isar/find_theorems.ML -%%DATADIR%%/src/Pure/Isar/instance.ML +%%DATADIR%%/src/Pure/Isar/expression.ML +%%DATADIR%%/src/Pure/Isar/isar.scala %%DATADIR%%/src/Pure/Isar/isar_cmd.ML +%%DATADIR%%/src/Pure/Isar/isar_document.ML +%%DATADIR%%/src/Pure/Isar/isar_document.scala %%DATADIR%%/src/Pure/Isar/isar_syn.ML %%DATADIR%%/src/Pure/Isar/local_defs.ML %%DATADIR%%/src/Pure/Isar/local_syntax.ML %%DATADIR%%/src/Pure/Isar/local_theory.ML %%DATADIR%%/src/Pure/Isar/locale.ML %%DATADIR%%/src/Pure/Isar/method.ML -%%DATADIR%%/src/Pure/Isar/net_rules.ML %%DATADIR%%/src/Pure/Isar/object_logic.ML %%DATADIR%%/src/Pure/Isar/obtain.ML %%DATADIR%%/src/Pure/Isar/outer_keyword.ML +%%DATADIR%%/src/Pure/Isar/outer_keyword.scala %%DATADIR%%/src/Pure/Isar/outer_lex.ML %%DATADIR%%/src/Pure/Isar/outer_parse.ML %%DATADIR%%/src/Pure/Isar/outer_syntax.ML +%%DATADIR%%/src/Pure/Isar/overloading.ML %%DATADIR%%/src/Pure/Isar/proof.ML %%DATADIR%%/src/Pure/Isar/proof_context.ML %%DATADIR%%/src/Pure/Isar/proof_display.ML -%%DATADIR%%/src/Pure/Isar/proof_history.ML +%%DATADIR%%/src/Pure/Isar/proof_node.ML %%DATADIR%%/src/Pure/Isar/rule_cases.ML %%DATADIR%%/src/Pure/Isar/rule_insts.ML -%%DATADIR%%/src/Pure/Isar/session.ML %%DATADIR%%/src/Pure/Isar/skip_proof.ML %%DATADIR%%/src/Pure/Isar/spec_parse.ML %%DATADIR%%/src/Pure/Isar/specification.ML -%%DATADIR%%/src/Pure/Isar/subclass.ML %%DATADIR%%/src/Pure/Isar/theory_target.ML %%DATADIR%%/src/Pure/Isar/toplevel.ML -%%DATADIR%%/src/Pure/ML-Systems/alice.ML +%%DATADIR%%/src/Pure/Isar/value_parse.ML %%DATADIR%%/src/Pure/ML-Systems/exn.ML +%%DATADIR%%/src/Pure/ML-Systems/install_pp_polyml-experimental.ML +%%DATADIR%%/src/Pure/ML-Systems/install_pp_polyml.ML +%%DATADIR%%/src/Pure/ML-Systems/ml_name_space.ML +%%DATADIR%%/src/Pure/ML-Systems/ml_pretty.ML %%DATADIR%%/src/Pure/ML-Systems/mosml.ML %%DATADIR%%/src/Pure/ML-Systems/multithreading.ML %%DATADIR%%/src/Pure/ML-Systems/multithreading_polyml.ML %%DATADIR%%/src/Pure/ML-Systems/overloading_smlnj.ML %%DATADIR%%/src/Pure/ML-Systems/polyml-4.1.3.ML %%DATADIR%%/src/Pure/ML-Systems/polyml-4.1.4.ML +%%DATADIR%%/src/Pure/ML-Systems/polyml-4.2.0.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-experimental.ML %%DATADIR%%/src/Pure/ML-Systems/polyml.ML -%%DATADIR%%/src/Pure/ML-Systems/poplogml.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/polyml_pp.ML %%DATADIR%%/src/Pure/ML-Systems/proper_int.ML %%DATADIR%%/src/Pure/ML-Systems/smlnj.ML +%%DATADIR%%/src/Pure/ML-Systems/system_shell.ML +%%DATADIR%%/src/Pure/ML-Systems/thread_dummy.ML %%DATADIR%%/src/Pure/ML-Systems/time_limit.ML +%%DATADIR%%/src/Pure/ML-Systems/universal.ML +%%DATADIR%%/src/Pure/ML-Systems/use_context.ML +%%DATADIR%%/src/Pure/ML/ml_antiquote.ML %%DATADIR%%/src/Pure/ML/ml_context.ML %%DATADIR%%/src/Pure/ML/ml_lex.ML %%DATADIR%%/src/Pure/ML/ml_parse.ML %%DATADIR%%/src/Pure/ML/ml_syntax.ML +%%DATADIR%%/src/Pure/ML/ml_test.ML +%%DATADIR%%/src/Pure/ML/ml_thms.ML %%DATADIR%%/src/Pure/Proof/extraction.ML %%DATADIR%%/src/Pure/Proof/proof_rewrite_rules.ML %%DATADIR%%/src/Pure/Proof/proof_syntax.ML @@ -3438,7 +4185,6 @@ %%DATADIR%%/src/Pure/ProofGeneral/pgip_tests.ML %%DATADIR%%/src/Pure/ProofGeneral/pgip_types.ML %%DATADIR%%/src/Pure/ProofGeneral/pgml.ML -%%DATADIR%%/src/Pure/ProofGeneral/pgml_isabelle.ML %%DATADIR%%/src/Pure/ProofGeneral/preferences.ML %%DATADIR%%/src/Pure/ProofGeneral/proof_general_emacs.ML %%DATADIR%%/src/Pure/ProofGeneral/proof_general_keywords.ML @@ -3456,19 +4202,27 @@ %%DATADIR%%/src/Pure/Syntax/syn_trans.ML %%DATADIR%%/src/Pure/Syntax/syntax.ML %%DATADIR%%/src/Pure/Syntax/type_ext.ML +%%DATADIR%%/src/Pure/System/isabelle_process.ML +%%DATADIR%%/src/Pure/System/isabelle_process.scala +%%DATADIR%%/src/Pure/System/isabelle_system.scala +%%DATADIR%%/src/Pure/System/isar.ML +%%DATADIR%%/src/Pure/System/session.ML %%DATADIR%%/src/Pure/Thy/html.ML %%DATADIR%%/src/Pure/Thy/latex.ML %%DATADIR%%/src/Pure/Thy/present.ML %%DATADIR%%/src/Pure/Thy/term_style.ML %%DATADIR%%/src/Pure/Thy/thm_deps.ML -%%DATADIR%%/src/Pure/Thy/thy_edit.ML %%DATADIR%%/src/Pure/Thy/thy_header.ML +%%DATADIR%%/src/Pure/Thy/thy_header.scala %%DATADIR%%/src/Pure/Thy/thy_info.ML %%DATADIR%%/src/Pure/Thy/thy_load.ML %%DATADIR%%/src/Pure/Thy/thy_output.ML +%%DATADIR%%/src/Pure/Thy/thy_syntax.ML %%DATADIR%%/src/Pure/Tools/ROOT.ML -%%DATADIR%%/src/Pure/Tools/invoke.ML +%%DATADIR%%/src/Pure/Tools/find_consts.ML +%%DATADIR%%/src/Pure/Tools/find_theorems.ML %%DATADIR%%/src/Pure/Tools/isabelle.xsd +%%DATADIR%%/src/Pure/Tools/isabelle_syntax.scala %%DATADIR%%/src/Pure/Tools/named_thms.ML %%DATADIR%%/src/Pure/Tools/xml_syntax.ML %%DATADIR%%/src/Pure/assumption.ML @@ -3478,13 +4232,16 @@ %%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/facts.ML %%DATADIR%%/src/Pure/goal.ML %%DATADIR%%/src/Pure/interpretation.ML +%%DATADIR%%/src/Pure/item_net.ML %%DATADIR%%/src/Pure/library.ML %%DATADIR%%/src/Pure/logic.ML %%DATADIR%%/src/Pure/meta_simplifier.ML @@ -3494,6 +4251,7 @@ %%DATADIR%%/src/Pure/name.ML %%DATADIR%%/src/Pure/net.ML %%DATADIR%%/src/Pure/old_goals.ML +%%DATADIR%%/src/Pure/old_term.ML %%DATADIR%%/src/Pure/pattern.ML %%DATADIR%%/src/Pure/primitive_defs.ML %%DATADIR%%/src/Pure/proofterm.ML @@ -3507,6 +4265,7 @@ %%DATADIR%%/src/Pure/tactic.ML %%DATADIR%%/src/Pure/tctical.ML %%DATADIR%%/src/Pure/term.ML +%%DATADIR%%/src/Pure/term_ord.ML %%DATADIR%%/src/Pure/term_subst.ML %%DATADIR%%/src/Pure/theory.ML %%DATADIR%%/src/Pure/thm.ML @@ -3514,18 +4273,6 @@ %%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 @@ -3547,7 +4294,6 @@ %%DATADIR%%/src/Sequents/modal.ML %%DATADIR%%/src/Sequents/prover.ML %%DATADIR%%/src/Sequents/simpdata.ML -%%DATADIR%%/src/TAGS %%DATADIR%%/src/Tools/Compute_Oracle/Compute_Oracle.thy %%DATADIR%%/src/Tools/Compute_Oracle/am.ML %%DATADIR%%/src/Tools/Compute_Oracle/am_compiler.ML @@ -3652,17 +4398,28 @@ %%DATADIR%%/src/Tools/Metis/src/problems2tptp.sml %%DATADIR%%/src/Tools/Metis/src/selftest.sml %%DATADIR%%/src/Tools/README +%%DATADIR%%/src/Tools/atomize_elim.ML +%%DATADIR%%/src/Tools/auto_solve.ML %%DATADIR%%/src/Tools/code/code_funcgr.ML +%%DATADIR%%/src/Tools/code/code_haskell.ML +%%DATADIR%%/src/Tools/code/code_ml.ML %%DATADIR%%/src/Tools/code/code_name.ML -%%DATADIR%%/src/Tools/code/code_package.ML +%%DATADIR%%/src/Tools/code/code_printer.ML %%DATADIR%%/src/Tools/code/code_target.ML %%DATADIR%%/src/Tools/code/code_thingol.ML +%%DATADIR%%/src/Tools/code/code_wellsorted.ML +%%DATADIR%%/src/Tools/coherent.ML +%%DATADIR%%/src/Tools/eqsubst.ML %%DATADIR%%/src/Tools/float.ML %%DATADIR%%/src/Tools/induct.ML +%%DATADIR%%/src/Tools/induct_tacs.ML +%%DATADIR%%/src/Tools/intuitionistic.ML %%DATADIR%%/src/Tools/nbe.ML -%%DATADIR%%/src/Tools/rat.ML -%%DATADIR%%/src/Tools/atomize_elim.ML +%%DATADIR%%/src/Tools/project_rule.ML +%%DATADIR%%/src/Tools/quickcheck.ML %%DATADIR%%/src/Tools/random_word.ML +%%DATADIR%%/src/Tools/rat.ML +%%DATADIR%%/src/Tools/value.ML %%DATADIR%%/src/ZF/AC.thy %%DATADIR%%/src/ZF/AC/AC15_WO6.thy %%DATADIR%%/src/ZF/AC/AC16_WO4.thy @@ -3721,6 +4478,7 @@ %%DATADIR%%/src/ZF/Constructible/Wellorderings.thy %%DATADIR%%/src/ZF/Constructible/document/root.bib %%DATADIR%%/src/ZF/Constructible/document/root.tex +%%DATADIR%%/src/ZF/Datatype_ZF.thy %%DATADIR%%/src/ZF/Epsilon.thy %%DATADIR%%/src/ZF/EquivClass.thy %%DATADIR%%/src/ZF/Finite.thy @@ -3749,11 +4507,17 @@ %%DATADIR%%/src/ZF/Induct/Term.thy %%DATADIR%%/src/ZF/Induct/Tree_Forest.thy %%DATADIR%%/src/ZF/Induct/document/root.tex +%%DATADIR%%/src/ZF/Inductive_ZF.thy %%DATADIR%%/src/ZF/InfDatatype.thy %%DATADIR%%/src/ZF/IntArith.thy +%%DATADIR%%/src/ZF/IntDiv_ZF.thy +%%DATADIR%%/src/ZF/Int_ZF.thy %%DATADIR%%/src/ZF/IsaMakefile +%%DATADIR%%/src/ZF/List_ZF.thy %%DATADIR%%/src/ZF/Main.thy +%%DATADIR%%/src/ZF/Main_ZF.thy %%DATADIR%%/src/ZF/Main_ZFC.thy +%%DATADIR%%/src/ZF/Nat_ZF.thy %%DATADIR%%/src/ZF/OrdQuant.thy %%DATADIR%%/src/ZF/Order.thy %%DATADIR%%/src/ZF/OrderArith.thy @@ -3829,13 +4593,6 @@ %%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 @@ -3862,6 +4619,7 @@ @dirrm %%DATADIR%%/src/Sequents @dirrm %%DATADIR%%/src/Pure/Tools @dirrm %%DATADIR%%/src/Pure/Thy +@dirrm %%DATADIR%%/src/Pure/System @dirrm %%DATADIR%%/src/Pure/Syntax @dirrm %%DATADIR%%/src/Pure/ProofGeneral @dirrm %%DATADIR%%/src/Pure/Proof @@ -3869,6 +4627,7 @@ @dirrm %%DATADIR%%/src/Pure/ML @dirrm %%DATADIR%%/src/Pure/Isar @dirrm %%DATADIR%%/src/Pure/General +@dirrm %%DATADIR%%/src/Pure/Concurrent @dirrm %%DATADIR%%/src/Pure @dirrm %%DATADIR%%/src/Provers/Arith @dirrm %%DATADIR%%/src/Provers @@ -3921,9 +4680,6 @@ @dirrm %%DATADIR%%/src/HOL/SizeChange @dirrm %%DATADIR%%/src/HOL/SET-Protocol/document @dirrm %%DATADIR%%/src/HOL/SET-Protocol -@dirrm %%DATADIR%%/src/HOL/Real/HahnBanach/document -@dirrm %%DATADIR%%/src/HOL/Real/HahnBanach -@dirrm %%DATADIR%%/src/HOL/Real @dirrm %%DATADIR%%/src/HOL/Prolog @dirrm %%DATADIR%%/src/HOL/NumberTheory/document @dirrm %%DATADIR%%/src/HOL/NumberTheory @@ -3931,6 +4687,9 @@ @dirrm %%DATADIR%%/src/HOL/Nominal @dirrm %%DATADIR%%/src/HOL/NanoJava/document @dirrm %%DATADIR%%/src/HOL/NanoJava +@dirrm %%DATADIR%%/src/HOL/NSA/document +@dirrm %%DATADIR%%/src/HOL/NSA/Examples +@dirrm %%DATADIR%%/src/HOL/NSA @dirrm %%DATADIR%%/src/HOL/Modelcheck @dirrm %%DATADIR%%/src/HOL/MicroJava/document @dirrm %%DATADIR%%/src/HOL/MicroJava/JVM @@ -3958,25 +4717,24 @@ @dirrm %%DATADIR%%/src/HOL/Import/Generate-HOLLight @dirrm %%DATADIR%%/src/HOL/Import/Generate-HOL @dirrm %%DATADIR%%/src/HOL/Import +@dirrm %%DATADIR%%/src/HOL/Imperative_HOL/ex +@dirrm %%DATADIR%%/src/HOL/Imperative_HOL @dirrm %%DATADIR%%/src/HOL/IOA @dirrm %%DATADIR%%/src/HOL/IMPP @dirrm %%DATADIR%%/src/HOL/IMP/document @dirrm %%DATADIR%%/src/HOL/IMP -@dirrm %%DATADIR%%/src/HOL/Hyperreal @dirrm %%DATADIR%%/src/HOL/HoareParallel/document @dirrm %%DATADIR%%/src/HOL/HoareParallel @dirrm %%DATADIR%%/src/HOL/Hoare/document @dirrm %%DATADIR%%/src/HOL/Hoare +@dirrm %%DATADIR%%/src/HOL/HahnBanach/document +@dirrm %%DATADIR%%/src/HOL/HahnBanach @dirrm %%DATADIR%%/src/HOL/Extraction/document @dirrm %%DATADIR%%/src/HOL/Extraction -@dirrm %%DATADIR%%/src/HOL/Complex/ex/document -@dirrm %%DATADIR%%/src/HOL/Complex/ex -@dirrm %%DATADIR%%/src/HOL/Complex/document -@dirrm %%DATADIR%%/src/HOL/Complex +@dirrm %%DATADIR%%/src/HOL/Decision_Procs/ex +@dirrm %%DATADIR%%/src/HOL/Decision_Procs @dirrm %%DATADIR%%/src/HOL/Bali/document @dirrm %%DATADIR%%/src/HOL/Bali -@dirrm %%DATADIR%%/src/HOL/AxClasses/Lattice -@dirrm %%DATADIR%%/src/HOL/AxClasses @dirrm %%DATADIR%%/src/HOL/Auth/document @dirrm %%DATADIR%%/src/HOL/Auth/Smartcard @dirrm %%DATADIR%%/src/HOL/Auth/Guard @@ -4001,16 +4759,15 @@ @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/fonts +@dirrm %%DATADIR%%/lib/classes @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 @@ -4018,6 +4775,7 @@ @dirrm %%DATADIR%%/heaps/%%HEAPSUBDIR%% @dirrm %%DATADIR%%/heaps @dirrm %%DATADIR%%/etc +@dirrm %%DATADIR%%/contrib/SystemOnTPTP @dirrm %%DATADIR%%/contrib @dirrm %%DATADIR%%/bin @dirrm %%DATADIR%% @@ -4107,6 +4865,8 @@ %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/MicroJava %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/MetisExamples/.session %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/MetisExamples +%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/Matrix/.session +%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/Matrix %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/Library/.session %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/Library %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/Lattice/.session @@ -4117,6 +4877,10 @@ %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/Isar_examples %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/Induct/.session %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/Induct +%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/Import/.session +%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/Import +%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/Imperative_HOL/.session +%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/Imperative_HOL %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/IOA/.session %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/IOA %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/IMPP/.session @@ -4127,6 +4891,10 @@ %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/HoareParallel %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/Hoare/.session %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/Hoare +%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/HahnBanach/.session +%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/HahnBanach +%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/HOL4/.session +%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/HOL4 %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/HOL-Word/Examples/.session %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/HOL-Word/Examples %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/HOL-Word/.session @@ -4135,29 +4903,25 @@ %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/HOL-Nominal/Examples %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/HOL-Nominal/.session %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/HOL-Nominal -%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex/.session -%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/HOL-Complex/ex -%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import/.session -%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/HOL-Complex/Import -%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/HOL-Complex/HahnBanach/.session -%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/HOL-Complex/HahnBanach -%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4/.session -%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL4 -%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix/.session -%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/HOL-Complex/HOL-Complex-Matrix -%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/HOL-Complex/.session -%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/HOL-Complex +%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/HOL-NSA/.session +%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/HOL-NSA %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/HOL-Algebra/.session %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/HOL-Algebra %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/Extraction/.session %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/Extraction +%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/Decision_Procs/.session +%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/Decision_Procs %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/Bali/.session %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/Bali -%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/AxClasses/.session -%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/AxClasses %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/Auth/.session %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/Auth %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL/.session +%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL-Plain/.session +%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL-Plain +%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL-Main/.session +%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL-Main +%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL-Base/.session +%%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL-Base %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/HOL %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/FOLP/ex/.session %%PORTDOCS%%@dirrm %%DOCSDIR%%/browser_info/FOLP/ex Index: files/patch-etc-settings =================================================================== RCS file: /home/ncvs/ports/math/isabelle/files/patch-etc-settings,v retrieving revision 1.5 diff -u -r1.5 patch-etc-settings --- files/patch-etc-settings 15 Aug 2008 04:33:04 -0000 1.5 +++ files/patch-etc-settings 18 Oct 2009 21:38:29 -0000 @@ -1,9 +1,13 @@ ---- 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. +--- etc/settings.orig 2009-10-09 10:34:33.000000000 +1100 ++++ etc/settings 2009-10-09 10:37:10.000000000 +1100 +@@ -11,55 +11,11 @@ + ### ML compiler settings (ESSENTIAL!) + ### +-# ML_HOME specifies the location of the actual compiler binaries. Do +-# not invent new ML system names unless you know what you are doing. +-# Only one of the sections below should be activated. +- -# Poly/ML 4.x/5.x (automated settings) -POLY_HOME="$(type -p poly)"; [ -n "$POLY_HOME" ] && POLY_HOME="$(dirname "$POLY_HOME")" -ML_PLATFORM=$("$ISABELLE_HOME/lib/scripts/polyml-platform") @@ -42,37 +46,23 @@ -#ML_OPTIONS="@SMLdebug=/dev/null" -#ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX") -#SMLNJ_CYGWIN_RUNTIME=1 +- +-# Moscow ML 2.00 (experimental!) +-#ML_SYSTEM=mosml +-#ML_HOME="/usr/local/mosml/bin" +-#ML_OPTIONS="" +-#ML_PLATFORM="" +- +ML_SYSTEM=%%ML_SYSTEM%% +ML_HOME=%%ML_HOME%% +ML_OPTIONS=%%ML_OPTIONS%% +ML_PLATFORM=%%ML_PLATFORM%% +ML_DBASE=%%ML_DBASE%% - # Moscow ML 2.00 (experimental!) - #ML_SYSTEM=mosml --#ML_HOME="/usr/local/mosml/bin" -+#ML_HOME="%%PREFIX%%/bin" - #ML_OPTIONS="" - #ML_PLATFORM="" - - # Alice 1.4 (experimental!) - #ML_SYSTEM=alice --#ML_HOME="/usr/local/alice/bin" -+#ML_HOME="%%PREFIX%%/bin" - #ML_OPTIONS="" - #ML_PLATFORM="" - - # Poplog/PML version 15.6/2.1 (experimental!) - #ML_SYSTEM=poplogml --#ML_HOME="/usr/local/poplog/current-poplog/bin" -+#ML_HOME="%%PREFIX%%/bin" - #ML_OPTIONS="-noinit" - #ML_SUFFIX=".psv" - #ML_PLATFORM="" - -- ### - ### Interactive sessions (cf. isatool tty) + ### JVM components (Scala or Java) +@@ -81,7 +37,7 @@ + ### Interactive sessions (cf. isabelle tty) ### -ISABELLE_LINE_EDITOR="" @@ -80,7 +70,16 @@ [ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)" [ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p ledit)" -@@ -154,7 +120,7 @@ +@@ -131,7 +87,7 @@ + ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools" + + # Location for temporary files (should be on a local file system). +-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER" ++ISABELLE_TMP_PREFIX="%%SYSTMPDIR%%/isabelle-$USER" + + # Heap input locations. ML system identifier is included in lookup. + ISABELLE_PATH="$ISABELLE_HOME_USER/heaps/$ISABELLE_IDENTIFIER:$ISABELLE_HOME/heaps" +@@ -157,7 +113,7 @@ ### # Where to look for docs (multiple dirs separated by ':'). @@ -89,29 +88,50 @@ # Preferred document format ISABELLE_DOC_FORMAT=pdf -@@ -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" \ -@@ -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" "") +@@ -191,9 +147,7 @@ + PROOFGENERAL_HOME=$(choosefrom \ + "$ISABELLE_HOME/contrib/ProofGeneral" \ + "$ISABELLE_HOME/../ProofGeneral" \ +- "/usr/local/ProofGeneral" \ +- "/usr/share/ProofGeneral" \ +- "/opt/ProofGeneral" \ ++ "%%PREFIX%%/%%EMACS_SITE_LISPDIR%%/ProofGeneral" \ + "") + + PROOFGENERAL_OPTIONS="" +@@ -211,9 +165,7 @@ + JEDIT_HOME=$(choosefrom \ + "$ISABELLE_HOME/contrib/jedit" \ + "$ISABELLE_HOME/../jedit" \ +- "/usr/local/jedit" \ +- "/usr/share/jedit" \ +- "/opt/jedit" \ ++ "%%JAVASHAREDIR%%/jedit" \ + "") + + JEDIT_JAVA_OPTIONS="" +@@ -231,17 +183,17 @@ + E_HOME=$(choosefrom \ + "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" \ + "$ISABELLE_HOME/../E/$ML_PLATFORM" \ +- "/usr/local/E" \ ++ "%%PREFIX%%/E" \ + "") + VAMPIRE_HOME=$(choosefrom \ + "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" \ + "$ISABELLE_HOME/../vampire/$ML_PLATFORM" \ +- "/usr/local/Vampire" \ ++ "%%PREFIX%%/Vampire" \ + "") + SPASS_HOME=$(choosefrom \ + "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" \ + "$ISABELLE_HOME/../spass/$ML_PLATFORM/bin" \ +- "/usr/local/SPASS" \ ++ "%%PREFIX%%/SPASS" \ + "") # HOL4 proof objects (cf. Isabelle/src/HOL/Import) - #HOL4_PROOFS="$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs" -@@ -224,26 +192,26 @@ +@@ -253,24 +205,24 @@ #SVC_MACHINE=sparc-sun-solaris # Mucke (mu-calculus model checker) @@ -129,8 +149,6 @@ # zChaff (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML) -#ZCHAFF_HOME=/usr/local/bin +#ZCHAFF_HOME=%%PREFIX%%/bin - #ZCHAFF_VERSION=2004.5.13 - #ZCHAFF_VERSION=2004.11.15 # BerkMin561 (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML) -#BERKMIN_HOME=/usr/local/bin Index: files/patch-lib-scripts-run_smlnj =================================================================== RCS file: /home/ncvs/ports/math/isabelle/files/patch-lib-scripts-run_smlnj,v retrieving revision 1.3 diff -u -r1.3 patch-lib-scripts-run_smlnj --- files/patch-lib-scripts-run_smlnj 15 Aug 2008 04:33:04 -0000 1.3 +++ files/patch-lib-scripts-run_smlnj 18 Oct 2009 21:38:29 -0000 @@ -1,6 +1,6 @@ ---- 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 @@ +--- lib/scripts/run-smlnj.orig 2009-10-08 20:50:08.000000000 +1100 ++++ lib/scripts/run-smlnj 2009-10-08 20:51:07.000000000 +1100 +@@ -38,11 +38,10 @@ ## compiler binaries @@ -13,7 +13,7 @@ -@@ -84,8 +83,7 @@ +@@ -83,8 +82,7 @@ ## fix heap file name and permissions if [ -n "$OUTFILE" ]; then Index: files/patch-src-HOL-Tools-atp_manager.ML =================================================================== RCS file: files/patch-src-HOL-Tools-atp_manager.ML diff -N files/patch-src-HOL-Tools-atp_manager.ML --- /dev/null 1 Jan 1970 00:00:00 -0000 +++ files/patch-src-HOL-Tools-atp_manager.ML 18 Oct 2009 21:38:29 -0000 @@ -0,0 +1,15 @@ +--- src/HOL/Tools/atp_manager.ML.orig 2009-10-18 10:37:58.000000000 +1100 ++++ src/HOL/Tools/atp_manager.ML 2009-10-18 10:39:46.000000000 +1100 +@@ -77,9 +77,9 @@ + fun ord ((a, _), (b, _)) = Time.compare (a, b); + ); + +-val lookup_thread = AList.lookup Thread.equal; +-val delete_thread = AList.delete Thread.equal; +-val update_thread = AList.update Thread.equal; ++fun lookup_thread x = AList.lookup Thread.equal x; ++fun delete_thread x = AList.delete Thread.equal x; ++fun update_thread x = AList.update Thread.equal x; + + + (* state of thread manager *) Index: files/patch-src-HOL-Tools-atp_wrapper.ML =================================================================== RCS file: files/patch-src-HOL-Tools-atp_wrapper.ML diff -N files/patch-src-HOL-Tools-atp_wrapper.ML --- /dev/null 1 Jan 1970 00:00:00 -0000 +++ files/patch-src-HOL-Tools-atp_wrapper.ML 18 Oct 2009 21:38:29 -0000 @@ -0,0 +1,18 @@ +--- src/HOL/Tools/atp_wrapper.ML.orig 2009-10-18 11:13:04.000000000 +1100 ++++ src/HOL/Tools/atp_wrapper.ML 2009-10-18 11:14:20.000000000 +1100 +@@ -112,13 +112,13 @@ + fun tptp_prover_opts max_new theory_const = + tptp_prover_opts_full max_new theory_const false; + +-val tptp_prover = tptp_prover_opts 60 true; ++fun tptp_prover x = tptp_prover_opts 60 true x; + + (*for structured proofs: prover must support TSTP*) + fun full_prover_opts max_new theory_const = + tptp_prover_opts_full max_new theory_const true; + +-val full_prover = full_prover_opts 60 true; ++fun full_prover x = full_prover_opts 60 true x; + + + (* Vampire *) Index: files/patch-src-HOL-Tools-int_arith.ML =================================================================== RCS file: files/patch-src-HOL-Tools-int_arith.ML diff -N files/patch-src-HOL-Tools-int_arith.ML --- /dev/null 1 Jan 1970 00:00:00 -0000 +++ files/patch-src-HOL-Tools-int_arith.ML 18 Oct 2009 21:38:29 -0000 @@ -0,0 +1,29 @@ +--- src/HOL/Tools/int_arith.ML.orig 2009-04-17 01:29:56.000000000 +1000 ++++ src/HOL/Tools/int_arith.ML 2009-10-17 19:35:35.000000000 +1100 +@@ -229,7 +229,7 @@ + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff 1 + val find_first_coeff = find_first_coeff [] +- val trans_tac = K Arith_Data.trans_tac ++ fun trans_tac _ = Arith_Data.trans_tac + + fun norm_tac ss = + ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) +@@ -308,7 +308,7 @@ + val dest_coeff = dest_coeff 1 + val left_distrib = @{thm combine_common_factor} RS trans + val prove_conv = Arith_Data.prove_conv_nohyps +- val trans_tac = K Arith_Data.trans_tac ++ fun trans_tac _ = Arith_Data.trans_tac + + fun norm_tac ss = + ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) +@@ -334,7 +334,7 @@ + val dest_coeff = dest_fcoeff 1 + val left_distrib = @{thm combine_common_factor} RS trans + val prove_conv = Arith_Data.prove_conv_nohyps +- val trans_tac = K Arith_Data.trans_tac ++ fun trans_tac _ = Arith_Data.trans_tac + + val norm_ss1a = norm_ss1 addsimps inverse_1s @ divide_simps + fun norm_tac ss = Index: files/patch-src-HOL-Tools-int_factor_simprocs.ML =================================================================== RCS file: files/patch-src-HOL-Tools-int_factor_simprocs.ML diff -N files/patch-src-HOL-Tools-int_factor_simprocs.ML --- /dev/null 1 Jan 1970 00:00:00 -0000 +++ files/patch-src-HOL-Tools-int_factor_simprocs.ML 18 Oct 2009 21:38:29 -0000 @@ -0,0 +1,65 @@ +--- src/HOL/Tools/int_factor_simprocs.ML.orig 2009-10-17 19:46:40.000000000 +1100 ++++ src/HOL/Tools/int_factor_simprocs.ML 2009-10-17 20:06:01.000000000 +1100 +@@ -29,7 +29,7 @@ + struct + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff 1 +- val trans_tac = K Arith_Data.trans_tac ++ fun trans_tac _ = Arith_Data.trans_tac + + val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s + val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps +@@ -249,7 +249,7 @@ + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff + val find_first = find_first_t [] +- val trans_tac = K Arith_Data.trans_tac ++ fun trans_tac _ = Arith_Data.trans_tac + val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac} + fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss)) + val simplify_meta_eq = cancel_simplify_meta_eq +@@ -261,7 +261,7 @@ + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_eq + val dest_bal = HOLogic.dest_bin "op =" Term.dummyT +- val simp_conv = K (K (SOME @{thm mult_cancel_left})) ++ fun simp_conv _ _ = SOME @{thm mult_cancel_left} + ); + + (*for ordered rings*) +@@ -290,7 +290,7 @@ + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binop @{const_name Divides.div} + val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT +- val simp_conv = K (K (SOME @{thm zdiv_zmult_zmult1_if})) ++ fun simp_conv _ _ = SOME @{thm zdiv_zmult_zmult1_if} + ); + + structure IntModCancelFactor = ExtractCommonTermFun +@@ -298,7 +298,7 @@ + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binop @{const_name Divides.mod} + val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} HOLogic.intT +- val simp_conv = K (K (SOME @{thm zmod_zmult_zmult1})) ++ fun simp_conv _ _ = SOME @{thm zmod_zmult_zmult1} + ); + + structure IntDvdCancelFactor = ExtractCommonTermFun +@@ -306,7 +306,7 @@ + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} + val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} Term.dummyT +- val simp_conv = K (K (SOME @{thm dvd_mult_cancel_left})) ++ fun simp_conv _ _ = SOME @{thm dvd_mult_cancel_left} + ); + + (*Version for all fields, including unordered ones (type complex).*) +@@ -315,7 +315,7 @@ + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binop @{const_name HOL.divide} + val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT +- val simp_conv = K (K (SOME @{thm mult_divide_mult_cancel_left_if})) ++ fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if} + ); + + val cancel_factors = Index: files/patch-src-HOL-Tools-nat_simprocs.ML =================================================================== RCS file: files/patch-src-HOL-Tools-nat_simprocs.ML diff -N files/patch-src-HOL-Tools-nat_simprocs.ML --- /dev/null 1 Jan 1970 00:00:00 -0000 +++ files/patch-src-HOL-Tools-nat_simprocs.ML 18 Oct 2009 21:38:30 -0000 @@ -0,0 +1,83 @@ +--- src/HOL/Tools/nat_simprocs.ML.orig 2009-10-17 19:48:52.000000000 +1100 ++++ src/HOL/Tools/nat_simprocs.ML 2009-10-18 09:59:34.000000000 +1100 +@@ -142,7 +142,7 @@ + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff + val find_first_coeff = find_first_coeff [] +- val trans_tac = K Arith_Data.trans_tac ++ fun trans_tac _ = Arith_Data.trans_tac + + val norm_ss1 = Int_Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ + [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac} +@@ -231,7 +231,7 @@ + val dest_coeff = dest_coeff + val left_distrib = @{thm left_add_mult_distrib} RS trans + val prove_conv = Arith_Data.prove_conv_nohyps +- val trans_tac = K Arith_Data.trans_tac ++ fun trans_tac _ = Arith_Data.trans_tac + + val norm_ss1 = Int_Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac} + val norm_ss2 = Int_Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac} +@@ -256,7 +256,7 @@ + struct + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff +- val trans_tac = K Arith_Data.trans_tac ++ fun trans_tac _ = Arith_Data.trans_tac + + val norm_ss1 = Int_Numeral_Simprocs.num_ss addsimps + numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac} +@@ -362,7 +362,7 @@ + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff + val find_first = find_first_t [] +- val trans_tac = K Arith_Data.trans_tac ++ fun trans_tac _ = Arith_Data.trans_tac + val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac} + fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss)) + val simplify_meta_eq = cancel_simplify_meta_eq +@@ -373,7 +373,7 @@ + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_eq + val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT +- val simp_conv = K(K (SOME @{thm nat_mult_eq_cancel_disj})) ++ fun simp_conv _ _ = SOME @{thm nat_mult_eq_cancel_disj} + ); + + structure LessCancelFactor = ExtractCommonTermFun +@@ -381,7 +381,7 @@ + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} + val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT +- val simp_conv = K(K (SOME @{thm nat_mult_less_cancel_disj})) ++ fun simp_conv _ _ = SOME @{thm nat_mult_less_cancel_disj} + ); + + structure LeCancelFactor = ExtractCommonTermFun +@@ -389,7 +389,7 @@ + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} + val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT +- val simp_conv = K(K (SOME @{thm nat_mult_le_cancel_disj})) ++ fun simp_conv _ _ = SOME @{thm nat_mult_le_cancel_disj} + ); + + structure DivideCancelFactor = ExtractCommonTermFun +@@ -397,7 +397,7 @@ + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binop @{const_name Divides.div} + val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT +- val simp_conv = K(K (SOME @{thm nat_mult_div_cancel_disj})) ++ fun simp_conv _ _ = SOME @{thm nat_mult_div_cancel_disj} + ); + + structure DvdCancelFactor = ExtractCommonTermFun +@@ -405,7 +405,7 @@ + val prove_conv = Arith_Data.prove_conv + val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} + val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT +- val simp_conv = K(K (SOME @{thm nat_mult_dvd_cancel_disj})) ++ fun simp_conv _ _ = SOME @{thm nat_mult_dvd_cancel_disj} + ); + + val cancel_factor = --- isabelle-2009.patch ends here --- >Release-Note: >Audit-Trail: >Unformatted:
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?200910182139.n9ILdXa3014275>