discontinued obsolete IsaMakefile and ROOT.ML files from the Isabelle distribution;
authorwenzelm
Tue Aug 07 23:43:05 2012 +0200 (2012-08-07)
changeset 48722a5e3ba7cbb2a
parent 48721 866f6d5baf4c
child 48723 0829e958f0aa
discontinued obsolete IsaMakefile and ROOT.ML files from the Isabelle distribution;
NEWS
doc-src/System/Thy/Misc.thy
doc-src/System/Thy/Presentation.thy
doc-src/System/Thy/document/Misc.tex
doc-src/System/Thy/document/Presentation.tex
src/CCL/IsaMakefile
src/CCL/ROOT.ML
src/CCL/ex/ROOT.ML
src/CTT/IsaMakefile
src/CTT/ROOT.ML
src/CTT/ex/ROOT.ML
src/Cube/IsaMakefile
src/Cube/ROOT.ML
src/FOL/IsaMakefile
src/FOL/ROOT.ML
src/FOL/ex/ROOT.ML
src/FOLP/IsaMakefile
src/FOLP/ROOT.ML
src/FOLP/ex/ROOT.ML
src/HOL/Algebra/ROOT.ML
src/HOL/Auth/ROOT.ML
src/HOL/Bali/ROOT.ML
src/HOL/Boogie/Examples/ROOT.ML
src/HOL/Boogie/ROOT.ML
src/HOL/Codegenerator_Test/ROOT.ML
src/HOL/Datatype_Benchmark/ROOT.ML
src/HOL/Decision_Procs/ROOT.ML
src/HOL/HOLCF/FOCUS/ROOT.ML
src/HOL/HOLCF/IMP/ROOT.ML
src/HOL/HOLCF/IOA/ABP/ROOT.ML
src/HOL/HOLCF/IOA/NTP/ROOT.ML
src/HOL/HOLCF/IOA/ROOT.ML
src/HOL/HOLCF/IOA/Storage/ROOT.ML
src/HOL/HOLCF/IOA/ex/ROOT.ML
src/HOL/HOLCF/IsaMakefile
src/HOL/HOLCF/Library/ROOT.ML
src/HOL/HOLCF/ROOT.ML
src/HOL/HOLCF/Tutorial/ROOT.ML
src/HOL/HOLCF/ex/ROOT.ML
src/HOL/Hahn_Banach/ROOT.ML
src/HOL/Hoare/ROOT.ML
src/HOL/Hoare_Parallel/ROOT.ML
src/HOL/IMP/ROOT.ML
src/HOL/IMPP/ROOT.ML
src/HOL/IOA/ROOT.ML
src/HOL/Imperative_HOL/ROOT.ML
src/HOL/Import/ROOT.ML
src/HOL/Induct/ROOT.ML
src/HOL/IsaMakefile
src/HOL/Isar_Examples/ROOT.ML
src/HOL/Lattice/ROOT.ML
src/HOL/Library/ROOT.ML
src/HOL/Matrix_LP/ROOT.ML
src/HOL/Metis_Examples/ROOT.ML
src/HOL/MicroJava/ROOT.ML
src/HOL/Mirabelle/ROOT.ML
src/HOL/Multivariate_Analysis/ROOT.ML
src/HOL/Mutabelle/ROOT.ML
src/HOL/NSA/Examples/ROOT.ML
src/HOL/NSA/ROOT.ML
src/HOL/NanoJava/ROOT.ML
src/HOL/Nitpick_Examples/ROOT.ML
src/HOL/Nominal/Examples/ROOT.ML
src/HOL/Nominal/ROOT.ML
src/HOL/Number_Theory/ROOT.ML
src/HOL/Old_Number_Theory/ROOT.ML
src/HOL/Predicate_Compile_Examples/ROOT.ML
src/HOL/Probability/ROOT.ML
src/HOL/Prolog/ROOT.ML
src/HOL/Proofs/Extraction/ROOT.ML
src/HOL/Proofs/Lambda/ROOT.ML
src/HOL/Proofs/ex/ROOT.ML
src/HOL/Quickcheck_Benchmark/ROOT.ML
src/HOL/Quickcheck_Examples/ROOT.ML
src/HOL/Quotient_Examples/ROOT.ML
src/HOL/ROOT.ML
src/HOL/Record_Benchmark/ROOT.ML
src/HOL/SET_Protocol/ROOT.ML
src/HOL/SMT_Examples/ROOT.ML
src/HOL/SPARK/Examples/ROOT.ML
src/HOL/SPARK/Manual/ROOT.ML
src/HOL/SPARK/ROOT.ML
src/HOL/Statespace/ROOT.ML
src/HOL/TLA/Buffer/ROOT.ML
src/HOL/TLA/Inc/ROOT.ML
src/HOL/TLA/Memory/ROOT.ML
src/HOL/TLA/ROOT.ML
src/HOL/TPTP/ROOT.ML
src/HOL/UNITY/ROOT.ML
src/HOL/Unix/ROOT.ML
src/HOL/Word/Examples/ROOT.ML
src/HOL/Word/ROOT.ML
src/HOL/ZF/ROOT.ML
src/HOL/ex/ROOT.ML
src/LCF/IsaMakefile
src/LCF/ROOT.ML
src/LCF/ex/ROOT.ML
src/Pure/IsaMakefile
src/Sequents/IsaMakefile
src/Sequents/LK/ROOT.ML
src/Sequents/ROOT.ML
src/Tools/WWW_Find/IsaMakefile
src/Tools/WWW_Find/ROOT.ML
src/ZF/AC/ROOT.ML
src/ZF/Coind/ROOT.ML
src/ZF/Constructible/ROOT.ML
src/ZF/IMP/ROOT.ML
src/ZF/Induct/ROOT.ML
src/ZF/IsaMakefile
src/ZF/ROOT.ML
src/ZF/Resid/ROOT.ML
src/ZF/UNITY/ROOT.ML
src/ZF/ex/ROOT.ML
     1.1 --- a/NEWS	Tue Aug 07 23:38:18 2012 +0200
     1.2 +++ b/NEWS	Tue Aug 07 23:43:05 2012 +0200
     1.3 @@ -80,6 +80,12 @@
     1.4  build" tool and its examples.  Eventual INCOMPATIBILITY, as isabelle
     1.5  usedir / make / makeall are rendered obsolete.
     1.6  
     1.7 +* Discontinued obsolete IsaMakefile and ROOT.ML files from the
     1.8 +Isabelle distribution, except for rudimentary src/HOL/IsaMakefile that
     1.9 +provides some traditional targets that invoke "isabelle build".  Note
    1.10 +that this is inefficient!  Applications of Isabelle/HOL involving
    1.11 +"isabelle make" should be upgraded to use "isabelle build" directly.
    1.12 +
    1.13  * Discontinued obsolete Isabelle/build script, it is superseded by the
    1.14  regular isabelle build tool.  For example:
    1.15  
     2.1 --- a/doc-src/System/Thy/Misc.thy	Tue Aug 07 23:38:18 2012 +0200
     2.2 +++ b/doc-src/System/Thy/Misc.thy	Tue Aug 07 23:43:05 2012 +0200
     2.3 @@ -222,15 +222,6 @@
     2.4  *}
     2.5  
     2.6  
     2.7 -subsubsection {* Examples *}
     2.8 -
     2.9 -text {*
    2.10 -  Refer to the @{verbatim IsaMakefile}s of the Isabelle distribution's
    2.11 -  object-logics as a model for your own developments.  For example,
    2.12 -  see @{file "~~/src/FOL/IsaMakefile"}.
    2.13 -*}
    2.14 -
    2.15 -
    2.16  section {* Make all logics *}
    2.17  
    2.18  text {* The @{tool_def makeall} tool applies Isabelle make to any
     3.1 --- a/doc-src/System/Thy/Presentation.thy	Tue Aug 07 23:38:18 2012 +0200
     3.2 +++ b/doc-src/System/Thy/Presentation.thy	Tue Aug 07 23:43:05 2012 +0200
     3.3 @@ -242,7 +242,7 @@
     3.4    meant to cover all of the sub-session directories at the same time
     3.5    (this is the deeper reasong why @{verbatim IsaMakefile} is not made
     3.6    part of the initial session directory created by @{tool mkdir}).
     3.7 -  See @{file "~~/src/HOL/IsaMakefile"} for a full-blown example.  *}
     3.8 +*}
     3.9  
    3.10  
    3.11  section {* Running Isabelle sessions \label{sec:tool-usedir} *}
    3.12 @@ -419,15 +419,6 @@
    3.13  *}
    3.14  
    3.15  
    3.16 -subsubsection {* Examples *}
    3.17 -
    3.18 -text {* Refer to the @{verbatim IsaMakefile}s of the Isabelle
    3.19 -  distribution's object-logics as a model for your own developments.
    3.20 -  For example, see @{file "~~/src/FOL/IsaMakefile"}.  The @{tool_ref
    3.21 -  mkdir} tool creates @{verbatim IsaMakefile}s with proper invocation
    3.22 -  of @{tool usedir} as well.  *}
    3.23 -
    3.24 -
    3.25  section {* Preparing Isabelle session documents
    3.26    \label{sec:tool-document} *}
    3.27  
     4.1 --- a/doc-src/System/Thy/document/Misc.tex	Tue Aug 07 23:38:18 2012 +0200
     4.2 +++ b/doc-src/System/Thy/document/Misc.tex	Tue Aug 07 23:43:05 2012 +0200
     4.3 @@ -262,17 +262,6 @@
     4.4  \end{isamarkuptext}%
     4.5  \isamarkuptrue%
     4.6  %
     4.7 -\isamarkupsubsubsection{Examples%
     4.8 -}
     4.9 -\isamarkuptrue%
    4.10 -%
    4.11 -\begin{isamarkuptext}%
    4.12 -Refer to the \verb|IsaMakefile|s of the Isabelle distribution's
    4.13 -  object-logics as a model for your own developments.  For example,
    4.14 -  see \verb|~~/src/FOL/IsaMakefile|.%
    4.15 -\end{isamarkuptext}%
    4.16 -\isamarkuptrue%
    4.17 -%
    4.18  \isamarkupsection{Make all logics%
    4.19  }
    4.20  \isamarkuptrue%
     5.1 --- a/doc-src/System/Thy/document/Presentation.tex	Tue Aug 07 23:38:18 2012 +0200
     5.2 +++ b/doc-src/System/Thy/document/Presentation.tex	Tue Aug 07 23:43:05 2012 +0200
     5.3 @@ -257,8 +257,7 @@
     5.4    manual editing of the generated \verb|IsaMakefile|, which is
     5.5    meant to cover all of the sub-session directories at the same time
     5.6    (this is the deeper reasong why \verb|IsaMakefile| is not made
     5.7 -  part of the initial session directory created by \hyperlink{tool.mkdir}{\mbox{\isa{\isatool{mkdir}}}}).
     5.8 -  See \verb|~~/src/HOL/IsaMakefile| for a full-blown example.%
     5.9 +  part of the initial session directory created by \hyperlink{tool.mkdir}{\mbox{\isa{\isatool{mkdir}}}}).%
    5.10  \end{isamarkuptext}%
    5.11  \isamarkuptrue%
    5.12  %
    5.13 @@ -430,18 +429,6 @@
    5.14  \end{isamarkuptext}%
    5.15  \isamarkuptrue%
    5.16  %
    5.17 -\isamarkupsubsubsection{Examples%
    5.18 -}
    5.19 -\isamarkuptrue%
    5.20 -%
    5.21 -\begin{isamarkuptext}%
    5.22 -Refer to the \verb|IsaMakefile|s of the Isabelle
    5.23 -  distribution's object-logics as a model for your own developments.
    5.24 -  For example, see \verb|~~/src/FOL/IsaMakefile|.  The \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatool{mkdir}}}} tool creates \verb|IsaMakefile|s with proper invocation
    5.25 -  of \hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}} as well.%
    5.26 -\end{isamarkuptext}%
    5.27 -\isamarkuptrue%
    5.28 -%
    5.29  \isamarkupsection{Preparing Isabelle session documents
    5.30    \label{sec:tool-document}%
    5.31  }
     6.1 --- a/src/CCL/IsaMakefile	Tue Aug 07 23:38:18 2012 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,48 +0,0 @@
     6.4 -#
     6.5 -# IsaMakefile for CCL
     6.6 -#
     6.7 -
     6.8 -## targets
     6.9 -
    6.10 -default: CCL
    6.11 -images: CCL
    6.12 -test: CCL-ex
    6.13 -all: images test
    6.14 -full: all
    6.15 -smlnj: all
    6.16 -
    6.17 -
    6.18 -## global settings
    6.19 -
    6.20 -SRC = $(ISABELLE_HOME)/src
    6.21 -OUT = $(ISABELLE_OUTPUT)
    6.22 -LOG = $(OUT)/log
    6.23 -
    6.24 -
    6.25 -## CCL
    6.26 -
    6.27 -CCL: FOL $(OUT)/CCL
    6.28 -
    6.29 -FOL:
    6.30 -	@cd $(SRC)/FOL; $(ISABELLE_TOOL) make FOL
    6.31 -
    6.32 -$(OUT)/FOL: FOL
    6.33 -
    6.34 -$(OUT)/CCL: $(OUT)/FOL CCL.thy Fix.thy Gfp.thy Hered.thy Lfp.thy ROOT.ML \
    6.35 -  Set.thy Term.thy Trancl.thy Type.thy Wfd.thy
    6.36 -	@$(ISABELLE_TOOL) usedir -b -r $(OUT)/FOL CCL
    6.37 -
    6.38 -
    6.39 -## CCL-ex
    6.40 -
    6.41 -CCL-ex: CCL $(LOG)/CCL-ex.gz
    6.42 -
    6.43 -$(LOG)/CCL-ex.gz: $(OUT)/CCL ex/Flag.thy ex/List.thy ex/Nat.thy ex/ROOT.ML \
    6.44 -  ex/Stream.thy
    6.45 -	@$(ISABELLE_TOOL) usedir $(OUT)/CCL ex
    6.46 -
    6.47 -
    6.48 -## clean
    6.49 -
    6.50 -clean:
    6.51 -	@rm -f $(OUT)/CCL $(LOG)/CCL.gz $(LOG)/CCL-ex.gz
     7.1 --- a/src/CCL/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,11 +0,0 @@
     7.4 -(*  Title:      CCL/ROOT.ML
     7.5 -    Author:     Martin Coen, Cambridge University Computer Laboratory
     7.6 -    Copyright   1993  University of Cambridge
     7.7 -
     7.8 -Classical Computational Logic based on First-Order Logic.
     7.9 -
    7.10 -A computational logic for an untyped functional language with
    7.11 -evaluation to weak head-normal form.
    7.12 -*)
    7.13 -
    7.14 -use_thys ["Wfd", "Fix"];
     8.1 --- a/src/CCL/ex/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,8 +0,0 @@
     8.4 -(*  Title:      CCL/ex/ROOT.ML
     8.5 -    Author:     Martin Coen, Cambridge University Computer Laboratory
     8.6 -    Copyright   1993  University of Cambridge
     8.7 -
     8.8 -Examples for Classical Computational Logic.
     8.9 -*)
    8.10 -
    8.11 -use_thys ["Nat", "List", "Stream", "Flag"];
     9.1 --- a/src/CTT/IsaMakefile	Tue Aug 07 23:38:18 2012 +0200
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,46 +0,0 @@
     9.4 -#
     9.5 -# IsaMakefile for CTT
     9.6 -#
     9.7 -
     9.8 -## targets
     9.9 -
    9.10 -default: CTT
    9.11 -images: CTT
    9.12 -test: CTT-ex
    9.13 -all: images test
    9.14 -full: all
    9.15 -smlnj: all
    9.16 -
    9.17 -
    9.18 -## global settings
    9.19 -
    9.20 -SRC = $(ISABELLE_HOME)/src
    9.21 -OUT = $(ISABELLE_OUTPUT)
    9.22 -LOG = $(OUT)/log
    9.23 -
    9.24 -
    9.25 -## CTT
    9.26 -
    9.27 -CTT: Pure $(OUT)/CTT
    9.28 -
    9.29 -Pure:
    9.30 -	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
    9.31 -
    9.32 -$(OUT)/CTT: $(OUT)/Pure $(SRC)/Provers/typedsimp.ML Arith.thy \
    9.33 -  Bool.thy CTT.thy Main.thy ROOT.ML rew.ML
    9.34 -	@$(ISABELLE_TOOL) usedir -b $(OUT)/Pure CTT
    9.35 -
    9.36 -
    9.37 -## CTT-ex
    9.38 -
    9.39 -CTT-ex: CTT $(LOG)/CTT-ex.gz
    9.40 -
    9.41 -$(LOG)/CTT-ex.gz: $(OUT)/CTT ex/ROOT.ML ex/Elimination.thy \
    9.42 -  ex/Equality.thy ex/Synthesis.thy ex/Typechecking.thy
    9.43 -	@$(ISABELLE_TOOL) usedir $(OUT)/CTT ex
    9.44 -
    9.45 -
    9.46 -## clean
    9.47 -
    9.48 -clean:
    9.49 -	@rm -f $(OUT)/CTT $(LOG)/CTT.gz $(LOG)/CTT-ex.gz
    10.1 --- a/src/CTT/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,7 +0,0 @@
    10.4 -(*  Title:      CTT/ROOT.ML
    10.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    10.6 -    Copyright   1991  University of Cambridge
    10.7 -*)
    10.8 -
    10.9 -use_thys ["Main"];
   10.10 -
    11.1 --- a/src/CTT/ex/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,8 +0,0 @@
    11.4 -(*  Title:      CTT/ex/ROOT.ML
    11.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    11.6 -    Copyright   1991  University of Cambridge
    11.7 -
    11.8 -Examples for Constructive Type Theory. 
    11.9 -*)
   11.10 -
   11.11 -use_thys ["Typechecking", "Elimination", "Equality", "Synthesis"];
    12.1 --- a/src/Cube/IsaMakefile	Tue Aug 07 23:38:18 2012 +0200
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,36 +0,0 @@
    12.4 -#
    12.5 -# IsaMakefile for Cube
    12.6 -#
    12.7 -
    12.8 -## targets
    12.9 -
   12.10 -default: Pure-Cube
   12.11 -images:
   12.12 -test: Pure-Cube
   12.13 -all: images test
   12.14 -full: all
   12.15 -smlnj: all
   12.16 -
   12.17 -
   12.18 -## global settings
   12.19 -
   12.20 -SRC = $(ISABELLE_HOME)/src
   12.21 -OUT = $(ISABELLE_OUTPUT)
   12.22 -LOG = $(OUT)/log
   12.23 -
   12.24 -
   12.25 -## Pure-Cube
   12.26 -
   12.27 -Pure-Cube: Pure $(LOG)/Pure-Cube.gz
   12.28 -
   12.29 -Pure:
   12.30 -	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
   12.31 -
   12.32 -$(LOG)/Pure-Cube.gz: $(OUT)/Pure Cube.thy Example.thy ROOT.ML
   12.33 -	@cd ..; $(ISABELLE_TOOL) usedir $(OUT)/Pure Cube
   12.34 -
   12.35 -
   12.36 -## clean
   12.37 -
   12.38 -clean:
   12.39 -	@rm -f $(LOG)/Pure-Cube.gz
    13.1 --- a/src/Cube/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,8 +0,0 @@
    13.4 -(*  Title:      Cube/ROOT.ML
    13.5 -    Author:     Tobias Nipkow
    13.6 -    Copyright   1992  University of Cambridge
    13.7 -
    13.8 -The Lambda-Cube a la Barendregt.
    13.9 -*)
   13.10 -
   13.11 -use_thys ["Example"];
    14.1 --- a/src/FOL/IsaMakefile	Tue Aug 07 23:38:18 2012 +0200
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,63 +0,0 @@
    14.4 -#
    14.5 -# IsaMakefile for FOL
    14.6 -#
    14.7 -
    14.8 -## targets
    14.9 -
   14.10 -default: FOL
   14.11 -images: FOL
   14.12 -test: FOL-ex
   14.13 -all: images test
   14.14 -full: all
   14.15 -smlnj: all
   14.16 -
   14.17 -
   14.18 -## global settings
   14.19 -
   14.20 -SRC = $(ISABELLE_HOME)/src
   14.21 -OUT = $(ISABELLE_OUTPUT)
   14.22 -LOG = $(OUT)/log
   14.23 -
   14.24 -
   14.25 -## FOL
   14.26 -
   14.27 -FOL: Pure $(OUT)/FOL
   14.28 -
   14.29 -Pure:
   14.30 -	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
   14.31 -
   14.32 -$(OUT)/Pure: Pure
   14.33 -
   14.34 -$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML				\
   14.35 -  $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML			\
   14.36 -  $(SRC)/Tools/case_product.ML $(SRC)/Tools/misc_legacy.ML		\
   14.37 -  $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/IsaPlanner/isand.ML	\
   14.38 -  $(SRC)/Tools/IsaPlanner/rw_tools.ML					\
   14.39 -  $(SRC)/Tools/IsaPlanner/rw_inst.ML $(SRC)/Tools/eqsubst.ML		\
   14.40 -  $(SRC)/Provers/hypsubst.ML $(SRC)/Tools/induct.ML			\
   14.41 -  $(SRC)/Tools/intuitionistic.ML $(SRC)/Tools/atomize_elim.ML		\
   14.42 -  $(SRC)/Tools/project_rule.ML $(SRC)/Provers/quantifier1.ML		\
   14.43 -  $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML			\
   14.44 -  document/root.tex fologic.ML intprover.ML simpdata.ML
   14.45 -	@$(ISABELLE_TOOL) usedir -p 2 -b $(OUT)/Pure FOL
   14.46 -
   14.47 -
   14.48 -## FOL-ex
   14.49 -
   14.50 -FOL-ex: FOL $(LOG)/FOL-ex.gz
   14.51 -
   14.52 -$(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy ex/If.thy		\
   14.53 -  ex/Nat.thy ex/Nat_Class.thy ex/Natural_Numbers.thy			\
   14.54 -  ex/Locale_Test/Locale_Test.thy ex/Locale_Test/Locale_Test1.thy	\
   14.55 -  ex/Locale_Test/Locale_Test2.thy ex/Locale_Test/Locale_Test3.thy	\
   14.56 -  ex/Miniscope.thy ex/Prolog.thy ex/ROOT.ML ex/Classical.thy		\
   14.57 -  ex/document/root.tex ex/Foundation.thy ex/Intuitionistic.thy		\
   14.58 -  ex/Intro.thy ex/Propositional_Int.thy ex/Propositional_Cla.thy	\
   14.59 -  ex/Quantifiers_Int.thy ex/Quantifiers_Cla.thy
   14.60 -	@$(ISABELLE_TOOL) usedir $(OUT)/FOL ex
   14.61 -
   14.62 -
   14.63 -## clean
   14.64 -
   14.65 -clean:
   14.66 -	@rm -f $(OUT)/FOL $(LOG)/FOL.gz $(LOG)/FOL-ex.gz
    15.1 --- a/src/FOL/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    15.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.3 @@ -1,3 +0,0 @@
    15.4 -(* First-Order Logic with Natural Deduction *)
    15.5 -
    15.6 -use_thys ["FOL"];
    16.1 --- a/src/FOL/ex/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    16.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.3 @@ -1,19 +0,0 @@
    16.4 -use_thys [
    16.5 -  "First_Order_Logic",
    16.6 -  "Natural_Numbers",
    16.7 -  "Intro",
    16.8 -  "Nat",
    16.9 -  "Nat_Class",
   16.10 -  "Foundation",
   16.11 -  "Prolog",
   16.12 -  "Intuitionistic",
   16.13 -  "Propositional_Int",
   16.14 -  "Quantifiers_Int",
   16.15 -  "Classical",
   16.16 -  "Propositional_Cla",
   16.17 -  "Quantifiers_Cla",
   16.18 -  "Miniscope",
   16.19 -  "If"
   16.20 -];
   16.21 -
   16.22 -no_document use_thy "Locale_Test/Locale_Test";
    17.1 --- a/src/FOLP/IsaMakefile	Tue Aug 07 23:38:18 2012 +0200
    17.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.3 @@ -1,48 +0,0 @@
    17.4 -#
    17.5 -# IsaMakefile for FOLP
    17.6 -#
    17.7 -
    17.8 -## targets
    17.9 -
   17.10 -default: FOLP
   17.11 -images: FOLP
   17.12 -test: FOLP-ex
   17.13 -all: images test
   17.14 -full: all
   17.15 -smlnj: all
   17.16 -
   17.17 -
   17.18 -## global settings
   17.19 -
   17.20 -SRC = $(ISABELLE_HOME)/src
   17.21 -OUT = $(ISABELLE_OUTPUT)
   17.22 -LOG = $(OUT)/log
   17.23 -
   17.24 -
   17.25 -## FOLP
   17.26 -
   17.27 -FOLP: Pure $(OUT)/FOLP
   17.28 -
   17.29 -Pure:
   17.30 -	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
   17.31 -
   17.32 -$(OUT)/FOLP: $(OUT)/Pure FOLP.thy IFOLP.thy ROOT.ML classical.ML	\
   17.33 -  hypsubst.ML intprover.ML simp.ML simpdata.ML $(SRC)/Tools/misc_legacy.ML
   17.34 -	@$(ISABELLE_TOOL) usedir -b $(OUT)/Pure FOLP
   17.35 -
   17.36 -
   17.37 -## FOLP-ex
   17.38 -
   17.39 -FOLP-ex: FOLP $(LOG)/FOLP-ex.gz
   17.40 -
   17.41 -$(LOG)/FOLP-ex.gz: $(OUT)/FOLP ex/ROOT.ML ex/Foundation.thy ex/If.thy	\
   17.42 -  ex/Intro.thy ex/Nat.thy ex/Intuitionistic.thy ex/Classical.thy	\
   17.43 -  ex/Propositional_Int.thy ex/Propositional_Cla.thy			\
   17.44 -  ex/Quantifiers_Int.thy ex/Quantifiers_Cla.thy
   17.45 -	@$(ISABELLE_TOOL) usedir $(OUT)/FOLP ex
   17.46 -
   17.47 -
   17.48 -## clean
   17.49 -
   17.50 -clean:
   17.51 -	@rm -f $(OUT)/FOLP $(LOG)/FOLP.gz $(LOG)/FOLP-ex.gz
    18.1 --- a/src/FOLP/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    18.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.3 @@ -1,11 +0,0 @@
    18.4 -(*  Title:      FOLP/ROOT.ML
    18.5 -    Author:     Martin Coen, Cambridge University Computer Laboratory
    18.6 -    Copyright   1993  University of Cambridge
    18.7 -
    18.8 -Modifed version of Lawrence Paulson's FOL that contains proof terms.
    18.9 -
   18.10 -Presence of unknown proof term means that matching does not behave as expected.
   18.11 -*)
   18.12 -
   18.13 -use_thys ["FOLP"];
   18.14 -
    19.1 --- a/src/FOLP/ex/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    19.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.3 @@ -1,19 +0,0 @@
    19.4 -(*  Title:      FOLP/ex/ROOT.ML
    19.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    19.6 -    Copyright   1992  University of Cambridge
    19.7 -
    19.8 -Examples for First-Order Logic. 
    19.9 -*)
   19.10 -
   19.11 -use_thys [
   19.12 -  "Intro",
   19.13 -  "Nat",
   19.14 -  "Foundation",
   19.15 -  "If",
   19.16 -  "Intuitionistic",
   19.17 -  "Classical",
   19.18 -  "Propositional_Int",
   19.19 -  "Quantifiers_Int",
   19.20 -  "Propositional_Cla",
   19.21 -  "Quantifiers_Cla"
   19.22 -];
    20.1 --- a/src/HOL/Algebra/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    20.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.3 @@ -1,35 +0,0 @@
    20.4 -(*  Author: Clemens Ballarin, started 24 September 1999
    20.5 -
    20.6 -The Isabelle Algebraic Library.
    20.7 -*)
    20.8 -
    20.9 -(* Preliminaries from set and number theory *)
   20.10 -no_document use_thys [
   20.11 -  "~~/src/HOL/Library/FuncSet",
   20.12 -  "~~/src/HOL/Old_Number_Theory/Primes",
   20.13 -  "~~/src/HOL/Library/Binomial",
   20.14 -  "~~/src/HOL/Library/Permutation"
   20.15 -];
   20.16 -
   20.17 -
   20.18 -(*** New development, based on explicit structures ***)
   20.19 -
   20.20 -use_thys [
   20.21 -  (* Groups *)
   20.22 -  "FiniteProduct",      (* Product operator for commutative groups *)
   20.23 -  "Sylow",              (* Sylow's theorem *)
   20.24 -  "Bij",                (* Automorphism Groups *)
   20.25 -
   20.26 -  (* Rings *)
   20.27 -  "Divisibility",       (* Rings *)
   20.28 -  "IntRing",            (* Ideals and residue classes *)
   20.29 -  "UnivPoly"            (* Polynomials *)
   20.30 -];
   20.31 -
   20.32 -
   20.33 -(*** Old development, based on axiomatic type classes ***)
   20.34 -
   20.35 -no_document use_thys [
   20.36 -  "abstract/Abstract",  (*The ring theory*)
   20.37 -  "poly/Polynomial"     (*The full theory*)
   20.38 -];
    21.1 --- a/src/HOL/Auth/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    21.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.3 @@ -1,7 +0,0 @@
    21.4 -use_thys [
    21.5 -  "Auth_Shared",
    21.6 -  "Auth_Public",
    21.7 -  "Smartcard/Auth_Smartcard",
    21.8 -  "Guard/Auth_Guard_Shared",
    21.9 -  "Guard/Auth_Guard_Public"
   21.10 -];
    22.1 --- a/src/HOL/Bali/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    22.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.3 @@ -1,1 +0,0 @@
    22.4 -use_thys ["AxExample", "AxSound", "AxCompl", "Trans"];
    23.1 --- a/src/HOL/Boogie/Examples/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    23.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.3 @@ -1,1 +0,0 @@
    23.4 -use_thys ["Boogie_Max_Stepwise", "Boogie_Max", "Boogie_Dijkstra", "VCC_Max"];
    24.1 --- a/src/HOL/Boogie/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    24.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    24.3 @@ -1,1 +0,0 @@
    24.4 -use_thys ["Boogie"];
    25.1 --- a/src/HOL/Codegenerator_Test/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    25.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.3 @@ -1,1 +0,0 @@
    25.4 -use_thys ["Generate", "Generate_Pretty", "RBT_Set_Test"];
    26.1 --- a/src/HOL/Datatype_Benchmark/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    26.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    26.3 @@ -1,8 +0,0 @@
    26.4 -(*  Title:      HOL/Datatype_Benchmark/ROOT.ML
    26.5 -
    26.6 -Some rather large datatype examples (from John Harrison).
    26.7 -*)
    26.8 -
    26.9 -Toplevel.timing := true;
   26.10 -
   26.11 -use_thys ["Brackin", "Instructions", "SML", "Verilog"];
    27.1 --- a/src/HOL/Decision_Procs/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    27.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    27.3 @@ -1,1 +0,0 @@
    27.4 -use_thys ["Decision_Procs"];
    28.1 --- a/src/HOL/HOLCF/FOCUS/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    28.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    28.3 @@ -1,1 +0,0 @@
    28.4 -use_thys ["Fstreams", "FOCUS", "Buffer_adm"];
    29.1 --- a/src/HOL/HOLCF/IMP/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    29.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    29.3 @@ -1,1 +0,0 @@
    29.4 -use_thys ["HoareEx"];
    30.1 --- a/src/HOL/HOLCF/IOA/ABP/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    30.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    30.3 @@ -1,8 +0,0 @@
    30.4 -(*  Title:      HOL/HOLCF/IOA/ABP/ROOT.ML
    30.5 -    Author:     Olaf Mueller
    30.6 -
    30.7 -This is the ROOT file for the Alternating Bit Protocol performed in
    30.8 -I/O-Automata.
    30.9 -*)
   30.10 -
   30.11 -use_thys ["Correctness"];
    31.1 --- a/src/HOL/HOLCF/IOA/NTP/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    31.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    31.3 @@ -1,9 +0,0 @@
    31.4 -(*  Title:      HOL/HOLCF/IOA/NTP/ROOT.ML
    31.5 -    Author:     Tobias Nipkow & Konrad Slind
    31.6 -
    31.7 -This is the ROOT file for a network transmission protocol (NTP
    31.8 -subdirectory), performed in the I/O automata formalization by Olaf
    31.9 -Mueller.
   31.10 -*)
   31.11 -
   31.12 -use_thys ["Correctness"];
    32.1 --- a/src/HOL/HOLCF/IOA/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    32.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    32.3 @@ -1,8 +0,0 @@
    32.4 -(*  Title:      HOL/HOLCF/IOA/ROOT.ML
    32.5 -    Author:     Olaf Mueller
    32.6 -
    32.7 -Formalization of a semantic model of I/O-Automata.  See README.html
    32.8 -for details.
    32.9 -*)
   32.10 -
   32.11 -use_thys ["meta_theory/Abstraction"];
    33.1 --- a/src/HOL/HOLCF/IOA/Storage/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    33.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    33.3 @@ -1,6 +0,0 @@
    33.4 -(*  Title:      HOL/HOLCF/IOA/Storage/ROOT.ML
    33.5 -    Author:     Olaf Mueller
    33.6 -
    33.7 -Memory storage case study.
    33.8 -*)
    33.9 -use_thys ["Correctness"];
    34.1 --- a/src/HOL/HOLCF/IOA/ex/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    34.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    34.3 @@ -1,5 +0,0 @@
    34.4 -(*  Title:      HOL/HOLCF/IOA/ex/ROOT.ML
    34.5 -    Author:     Olaf Mueller
    34.6 -*)
    34.7 -
    34.8 -use_thys ["TrivEx", "TrivEx2"];
    35.1 --- a/src/HOL/HOLCF/IsaMakefile	Tue Aug 07 23:38:18 2012 +0200
    35.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    35.3 @@ -1,234 +0,0 @@
    35.4 -#
    35.5 -# IsaMakefile for HOLCF
    35.6 -#
    35.7 -
    35.8 -## targets
    35.9 -
   35.10 -default: HOLCF
   35.11 -images: HOLCF IOA
   35.12 -test: \
   35.13 -  HOLCF-FOCUS \
   35.14 -  HOLCF-IMP \
   35.15 -  HOLCF-Library \
   35.16 -  HOLCF-Tutorial \
   35.17 -  HOLCF-ex \
   35.18 -  IOA-ABP \
   35.19 -  IOA-NTP \
   35.20 -  IOA-Storage \
   35.21 -  IOA-ex
   35.22 -all: images test
   35.23 -full: all
   35.24 -
   35.25 -
   35.26 -## global settings
   35.27 -
   35.28 -SRC = $(ISABELLE_HOME)/src
   35.29 -OUT = $(ISABELLE_OUTPUT)
   35.30 -LOG = $(OUT)/log
   35.31 -
   35.32 -
   35.33 -## HOLCF
   35.34 -
   35.35 -HOLCF: HOL $(OUT)/HOLCF
   35.36 -
   35.37 -HOL:
   35.38 -	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
   35.39 -
   35.40 -$(OUT)/HOLCF: $(OUT)/HOL \
   35.41 -  ROOT.ML \
   35.42 -  Adm.thy \
   35.43 -  Algebraic.thy \
   35.44 -  Bifinite.thy \
   35.45 -  Cfun.thy \
   35.46 -  Compact_Basis.thy \
   35.47 -  Completion.thy \
   35.48 -  Cont.thy \
   35.49 -  ConvexPD.thy \
   35.50 -  Cpodef.thy \
   35.51 -  Cprod.thy \
   35.52 -  Discrete.thy \
   35.53 -  Deflation.thy \
   35.54 -  Domain.thy \
   35.55 -  Domain_Aux.thy \
   35.56 -  Fixrec.thy \
   35.57 -  Fix.thy \
   35.58 -  Fun_Cpo.thy \
   35.59 -  HOLCF.thy \
   35.60 -  Lift.thy \
   35.61 -  LowerPD.thy \
   35.62 -  Map_Functions.thy \
   35.63 -  One.thy \
   35.64 -  Pcpo.thy \
   35.65 -  Plain_HOLCF.thy \
   35.66 -  Porder.thy \
   35.67 -  Powerdomains.thy \
   35.68 -  Product_Cpo.thy \
   35.69 -  Representable.thy \
   35.70 -  Sfun.thy \
   35.71 -  Sprod.thy \
   35.72 -  Ssum.thy \
   35.73 -  Tr.thy \
   35.74 -  Universal.thy \
   35.75 -  UpperPD.thy \
   35.76 -  Up.thy \
   35.77 -  Tools/cont_consts.ML \
   35.78 -  Tools/cont_proc.ML \
   35.79 -  Tools/holcf_library.ML \
   35.80 -  Tools/Domain/domain.ML \
   35.81 -  Tools/Domain/domain_axioms.ML \
   35.82 -  Tools/Domain/domain_constructors.ML \
   35.83 -  Tools/Domain/domain_induction.ML \
   35.84 -  Tools/Domain/domain_isomorphism.ML \
   35.85 -  Tools/Domain/domain_take_proofs.ML \
   35.86 -  Tools/cpodef.ML \
   35.87 -  Tools/domaindef.ML \
   35.88 -  Tools/fixrec.ML \
   35.89 -  document/root.tex
   35.90 -	@$(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOLCF
   35.91 -
   35.92 -
   35.93 -## HOLCF-Tutorial
   35.94 -
   35.95 -HOLCF-Tutorial: HOLCF $(LOG)/HOLCF-Tutorial.gz
   35.96 -
   35.97 -$(LOG)/HOLCF-Tutorial.gz: $(OUT)/HOLCF \
   35.98 -  Tutorial/Domain_ex.thy \
   35.99 -  Tutorial/Fixrec_ex.thy \
  35.100 -  Tutorial/New_Domain.thy \
  35.101 -  Tutorial/document/root.tex \
  35.102 -  Tutorial/ROOT.ML
  35.103 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Tutorial
  35.104 -
  35.105 -
  35.106 -## HOLCF-Library
  35.107 -
  35.108 -HOLCF-Library: HOLCF $(LOG)/HOLCF-Library.gz
  35.109 -
  35.110 -$(LOG)/HOLCF-Library.gz: $(OUT)/HOLCF \
  35.111 -  Library/Defl_Bifinite.thy \
  35.112 -  Library/Bool_Discrete.thy \
  35.113 -  Library/Char_Discrete.thy \
  35.114 -  Library/HOL_Cpo.thy \
  35.115 -  Library/Int_Discrete.thy \
  35.116 -  Library/List_Cpo.thy \
  35.117 -  Library/List_Predomain.thy \
  35.118 -  Library/Nat_Discrete.thy \
  35.119 -  Library/Option_Cpo.thy \
  35.120 -  Library/Stream.thy \
  35.121 -  Library/Sum_Cpo.thy \
  35.122 -  Library/HOLCF_Library.thy \
  35.123 -  Library/ROOT.ML
  35.124 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Library
  35.125 -
  35.126 -
  35.127 -## HOLCF-IMP
  35.128 -
  35.129 -HOLCF-IMP: HOLCF $(LOG)/HOLCF-IMP.gz
  35.130 -
  35.131 -$(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF IMP/HoareEx.thy \
  35.132 -  IMP/Denotational.thy IMP/ROOT.ML IMP/document/root.tex
  35.133 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF IMP
  35.134 -
  35.135 -
  35.136 -## HOLCF-ex
  35.137 -
  35.138 -HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz
  35.139 -
  35.140 -$(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF \
  35.141 -  ../Library/Extended_Nat.thy \
  35.142 -  ex/Concurrency_Monad.thy \
  35.143 -  ex/Dagstuhl.thy \
  35.144 -  ex/Dnat.thy \
  35.145 -  ex/Domain_Proofs.thy \
  35.146 -  ex/Fix2.thy \
  35.147 -  ex/Focus_ex.thy \
  35.148 -  ex/Hoare.thy \
  35.149 -  ex/Letrec.thy \
  35.150 -  ex/Loop.thy \
  35.151 -  ex/Pattern_Match.thy \
  35.152 -  ex/Powerdomain_ex.thy \
  35.153 -  ex/ROOT.ML
  35.154 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF ex
  35.155 -
  35.156 -
  35.157 -## HOLCF-FOCUS
  35.158 -
  35.159 -HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz
  35.160 -
  35.161 -$(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF \
  35.162 -  Library/Stream.thy \
  35.163 -  FOCUS/Fstreams.thy \
  35.164 -  FOCUS/Fstream.thy FOCUS/FOCUS.thy \
  35.165 -  FOCUS/Stream_adm.thy ../Library/Continuity.thy \
  35.166 -  FOCUS/Buffer.thy FOCUS/Buffer_adm.thy
  35.167 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF FOCUS
  35.168 -
  35.169 -## IOA
  35.170 -
  35.171 -IOA: HOLCF $(OUT)/IOA
  35.172 -
  35.173 -$(OUT)/IOA: $(OUT)/HOLCF IOA/ROOT.ML IOA/meta_theory/Traces.thy        \
  35.174 -  IOA/meta_theory/Asig.thy IOA/meta_theory/CompoScheds.thy	       \
  35.175 -  IOA/meta_theory/CompoTraces.thy IOA/meta_theory/Seq.thy	       \
  35.176 -  IOA/meta_theory/RefCorrectness.thy IOA/meta_theory/Automata.thy      \
  35.177 -  IOA/meta_theory/ShortExecutions.thy IOA/meta_theory/IOA.thy	       \
  35.178 -  IOA/meta_theory/Sequence.thy IOA/meta_theory/CompoExecs.thy	       \
  35.179 -  IOA/meta_theory/RefMappings.thy IOA/meta_theory/Compositionality.thy \
  35.180 -  IOA/meta_theory/TL.thy IOA/meta_theory/TLS.thy		       \
  35.181 -  IOA/meta_theory/LiveIOA.thy IOA/meta_theory/Pred.thy		       \
  35.182 -  IOA/meta_theory/Abstraction.thy IOA/meta_theory/Simulations.thy      \
  35.183 -  IOA/meta_theory/SimCorrectness.thy
  35.184 -	@cd IOA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOLCF IOA
  35.185 -
  35.186 -
  35.187 -## IOA-ABP
  35.188 -
  35.189 -IOA-ABP: IOA $(LOG)/IOA-ABP.gz
  35.190 -
  35.191 -$(LOG)/IOA-ABP.gz: $(OUT)/IOA IOA/ABP/Abschannel.thy \
  35.192 -  IOA/ABP/Abschannel_finite.thy IOA/ABP/Action.thy \
  35.193 -  IOA/ABP/Check.ML IOA/ABP/Correctness.thy \
  35.194 -  IOA/ABP/Env.thy IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy \
  35.195 -  IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \
  35.196 -  IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy IOA/ABP/Sender.thy \
  35.197 -  IOA/ABP/Spec.thy
  35.198 -	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ABP
  35.199 -
  35.200 -## IOA-NTP
  35.201 -
  35.202 -IOA-NTP: IOA $(LOG)/IOA-NTP.gz
  35.203 -
  35.204 -$(LOG)/IOA-NTP.gz: $(OUT)/IOA \
  35.205 -  IOA/NTP/Abschannel.thy IOA/NTP/Action.thy IOA/NTP/Correctness.thy \
  35.206 -  IOA/NTP/Impl.thy IOA/NTP/Lemmas.thy IOA/NTP/Multiset.thy \
  35.207 -  IOA/NTP/Packet.thy IOA/NTP/ROOT.ML IOA/NTP/Receiver.thy IOA/NTP/Sender.thy \
  35.208 -  IOA/NTP/Spec.thy
  35.209 -	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA NTP
  35.210 -
  35.211 -
  35.212 -## IOA-Storage
  35.213 -
  35.214 -IOA-Storage: IOA $(LOG)/IOA-Storage.gz
  35.215 -
  35.216 -$(LOG)/IOA-Storage.gz: $(OUT)/IOA IOA/Storage/Action.thy \
  35.217 -  IOA/Storage/Correctness.thy IOA/Storage/Impl.thy \
  35.218 -  IOA/Storage/ROOT.ML IOA/Storage/Spec.thy
  35.219 -	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA Storage
  35.220 -
  35.221 -
  35.222 -## IOA-ex
  35.223 -
  35.224 -IOA-ex: IOA $(LOG)/IOA-ex.gz
  35.225 -
  35.226 -$(LOG)/IOA-ex.gz: $(OUT)/IOA IOA/ex/ROOT.ML IOA/ex/TrivEx.thy IOA/ex/TrivEx2.thy
  35.227 -	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ex
  35.228 -
  35.229 -
  35.230 -## clean
  35.231 -
  35.232 -clean:
  35.233 -	@rm -f $(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz	\
  35.234 -	  $(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA	\
  35.235 -	  $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz	\
  35.236 -	  $(LOG)/IOA-Storage.gz $(LOG)/HOLCF-Library.gz		\
  35.237 -	  $(LOG)/IOA-ex.gz $(LOG)/HOLCF-Tutorial.gz
    36.1 --- a/src/HOL/HOLCF/Library/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    36.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    36.3 @@ -1,1 +0,0 @@
    36.4 -use_thys ["HOLCF_Library"];
    37.1 --- a/src/HOL/HOLCF/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    37.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    37.3 @@ -1,9 +0,0 @@
    37.4 -(*  Title:      HOL/HOLCF/ROOT.ML
    37.5 -    Author:     Franz Regensburger
    37.6 -
    37.7 -HOLCF -- a semantic extension of HOL by the LCF logic.
    37.8 -*)
    37.9 -
   37.10 -no_document use_thys ["~~/src/HOL/Library/Nat_Bijection", "~~/src/HOL/Library/Countable"];
   37.11 -
   37.12 -use_thys ["Plain_HOLCF", "Fixrec", "HOLCF"];
    38.1 --- a/src/HOL/HOLCF/Tutorial/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    38.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    38.3 @@ -1,1 +0,0 @@
    38.4 -use_thys ["Domain_ex", "Fixrec_ex", "New_Domain"];
    39.1 --- a/src/HOL/HOLCF/ex/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    39.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    39.3 @@ -1,10 +0,0 @@
    39.4 -(*  Title:      HOL/HOLCF/ex/ROOT.ML
    39.5 -
    39.6 -Misc HOLCF examples.
    39.7 -*)
    39.8 -
    39.9 -use_thys ["Dnat", "Dagstuhl", "Focus_ex", "Fix2", "Hoare",
   39.10 -  "Concurrency_Monad",
   39.11 -  "Loop", "Powerdomain_ex", "Domain_Proofs",
   39.12 -  "Letrec",
   39.13 -  "Pattern_Match"];
    40.1 --- a/src/HOL/Hahn_Banach/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    40.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    40.3 @@ -1,7 +0,0 @@
    40.4 -(*  Title:      HOL/Hahn_Banach/ROOT.ML
    40.5 -    Author:     Gertrud Bauer, TU Munich
    40.6 -
    40.7 -The Hahn-Banach theorem for real vector spaces (Isabelle/Isar).
    40.8 -*)
    40.9 -
   40.10 -use_thys ["Hahn_Banach"];
    41.1 --- a/src/HOL/Hoare/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    41.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    41.3 @@ -1,2 +0,0 @@
    41.4 -
    41.5 -use_thy "Hoare";
    42.1 --- a/src/HOL/Hoare_Parallel/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    42.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    42.3 @@ -1,1 +0,0 @@
    42.4 -use_thys ["Hoare_Parallel"];
    43.1 --- a/src/HOL/IMP/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    43.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    43.3 @@ -1,39 +0,0 @@
    43.4 -no_document use_thys
    43.5 -  ["~~/src/HOL/ex/Interpretation_with_Defs",
    43.6 -   "~~/src/HOL/Library/While_Combinator",
    43.7 -   "~~/src/HOL/Library/Char_ord", "~~/src/HOL/Library/List_lexord"
    43.8 -  ];
    43.9 -
   43.10 -use_thys
   43.11 -["BExp",
   43.12 - "ASM",
   43.13 - "Small_Step",
   43.14 - "Denotation",
   43.15 - "Comp_Rev",
   43.16 - "Poly_Types",
   43.17 - "Sec_Typing",
   43.18 - "Sec_TypingT",
   43.19 - "Def_Ass_Sound_Big",
   43.20 - "Def_Ass_Sound_Small",
   43.21 - "Live",
   43.22 - "Live_True",
   43.23 - "Hoare_Examples",
   43.24 - "VC",
   43.25 - "HoareT",
   43.26 - "Collecting1",
   43.27 - "Collecting_list",
   43.28 - "Abs_Int_Tests",
   43.29 - "Abs_Int1_parity",
   43.30 - "Abs_Int1_const",
   43.31 - "Abs_Int3",
   43.32 - "Abs_Int_ITP/Abs_Int1_parity_ITP",
   43.33 - "Abs_Int_ITP/Abs_Int1_const_ITP",
   43.34 - "Abs_Int_ITP/Abs_Int3_ITP",
   43.35 - "Abs_Int_Den/Abs_Int_den2",
   43.36 - "Procs_Dyn_Vars_Dyn",
   43.37 - "Procs_Stat_Vars_Dyn",
   43.38 - "Procs_Stat_Vars_Stat",
   43.39 - "C_like",
   43.40 - "OO",
   43.41 - "Fold"
   43.42 -];
    44.1 --- a/src/HOL/IMPP/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    44.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    44.3 @@ -1,6 +0,0 @@
    44.4 -(*  Title:      HOL/IMPP/ROOT.ML
    44.5 -    Author:     David von Oheimb
    44.6 -    Copyright   1999 TUM
    44.7 -*)
    44.8 -
    44.9 -use_thys ["EvenOdd"];
    45.1 --- a/src/HOL/IOA/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    45.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    45.3 @@ -1,27 +0,0 @@
    45.4 -(*  Title:      HOL/IOA/ROOT.ML
    45.5 -    Author:     Tobias Nipkow & Konrad Slind
    45.6 -    Copyright   1994  TU Muenchen
    45.7 -
    45.8 -This is the ROOT file for the meta theory of I/O-Automata.
    45.9 -
   45.10 -@inproceedings{Nipkow-Slind-IOA,
   45.11 -author={Tobias Nipkow and Konrad Slind},
   45.12 -title={{I/O} Automata in {Isabelle/HOL}},
   45.13 -booktitle={Proc.\ TYPES Workshop 1994},
   45.14 -publisher=Springer,
   45.15 -series=LNCS,
   45.16 -note={To appear}}
   45.17 -ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz
   45.18 -
   45.19 -and
   45.20 -
   45.21 -@inproceedings{Mueller-Nipkow,
   45.22 -author={Olaf M\"uller and Tobias Nipkow},
   45.23 -title={Combining Model Checking and Deduction for {I/O}-Automata},
   45.24 -booktitle={Proc.\ TACAS Workshop},
   45.25 -organization={Aarhus University, BRICS report},
   45.26 -year=1995}
   45.27 -ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
   45.28 -*)
   45.29 -
   45.30 -use_thys ["Solve"];
    46.1 --- a/src/HOL/Imperative_HOL/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    46.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    46.3 @@ -1,7 +0,0 @@
    46.4 -no_document use_thys [
    46.5 -  "~~/src/HOL/Library/Countable",
    46.6 -  "~~/src/HOL/Library/Monad_Syntax",
    46.7 -  "~~/src/HOL/Library/Code_Natural",
    46.8 -  "~~/src/HOL/Library/LaTeXsugar"];
    46.9 -
   46.10 -use_thys ["Imperative_HOL_ex"];
    47.1 --- a/src/HOL/Import/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    47.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    47.3 @@ -1,5 +0,0 @@
    47.4 -use_thy "HOL_Light_Maps";
    47.5 -
    47.6 -if getenv "HOL_LIGHT_BUNDLE" <> ""
    47.7 -then use_thy "HOL_Light_Import"
    47.8 -else ()
    48.1 --- a/src/HOL/Induct/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    48.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    48.3 @@ -1,5 +0,0 @@
    48.4 -Unsynchronized.setmp quick_and_dirty true
    48.5 -  use_thys ["Common_Patterns"];
    48.6 -
    48.7 -use_thys ["QuoDataType", "QuoNestedDataType", "Term", "SList",
    48.8 -  "ABexp", "Tree", "Ordinals", "Sigma_Algebra", "Comb", "PropLog", "Com"];
    49.1 --- a/src/HOL/IsaMakefile	Tue Aug 07 23:38:18 2012 +0200
    49.2 +++ b/src/HOL/IsaMakefile	Tue Aug 07 23:43:05 2012 +0200
    49.3 @@ -1,1883 +1,36 @@
    49.4 -#
    49.5 -# IsaMakefile for HOL
    49.6  #
    49.7 -
    49.8 -## targets
    49.9 +# approximative IsaMakefile for legacy applications
   49.10 +#
   49.11  
   49.12  default: HOL
   49.13  
   49.14 -images: \
   49.15 -  HOL \
   49.16 -  HOL-Library \
   49.17 -  HOL-Algebra \
   49.18 -  HOL-Boogie \
   49.19 -  HOL-IMP \
   49.20 -  HOL-Multivariate_Analysis \
   49.21 -  HOL-NSA \
   49.22 -  HOL-Nominal \
   49.23 -  HOL-Proofs \
   49.24 -  HOL-SPARK \
   49.25 -  HOL-Word \
   49.26 -  HOLCF \
   49.27 -  IOA \
   49.28 -  TLA \
   49.29 -  HOL-Base \
   49.30 -  HOL-Main \
   49.31 -  HOL-Plain
   49.32 +clean:
   49.33 +	-@$(ISABELLE_TOOL) build -a -n -c
   49.34  
   49.35 -#Note: keep targets sorted
   49.36 -test: \
   49.37 -  HOL-Auth \
   49.38 -  HOL-Bali \
   49.39 -  HOL-Boogie-Examples \
   49.40 -  HOL-Hahn_Banach \
   49.41 -  HOL-Hoare \
   49.42 -  HOL-Hoare_Parallel \
   49.43 -      HOLCF-FOCUS \
   49.44 -      HOLCF-IMP \
   49.45 -      HOLCF-Library \
   49.46 -      HOLCF-Tutorial \
   49.47 -      HOLCF-ex \
   49.48 -  HOL-IMPP \
   49.49 -  HOL-Import \
   49.50 -  HOL-IOA \
   49.51 -      IOA-ABP \
   49.52 -      IOA-NTP \
   49.53 -      IOA-Storage \
   49.54 -      IOA-ex \
   49.55 -  HOL-Imperative_HOL \
   49.56 -  HOL-Induct \
   49.57 -  HOL-Isar_Examples \
   49.58 -  HOL-Lattice \
   49.59 -  HOL-Library-Codegenerator_Test \
   49.60 -  HOL-Matrix_LP \
   49.61 -  HOL-Metis_Examples \
   49.62 -  HOL-MicroJava \
   49.63 -  HOL-Mirabelle \
   49.64 -  HOL-Mutabelle \
   49.65 -  HOL-NanoJava \
   49.66 -  HOL-Nitpick_Examples \
   49.67 -  HOL-NSA-Examples \
   49.68 -  HOL-Number_Theory \
   49.69 -  HOL-Old_Number_Theory \
   49.70 -  HOL-Quickcheck_Examples \
   49.71 -  HOL-Quotient_Examples \
   49.72 -  HOL-Predicate_Compile_Examples \
   49.73 -  HOL-Prolog \
   49.74 -  HOL-Proofs-ex \
   49.75 -  HOL-Proofs-Lambda \
   49.76 -  HOL-SET_Protocol \
   49.77 -  HOL-SPARK-Examples \
   49.78 -  HOL-SPARK-Manual \
   49.79 -  HOL-Word-SMT_Examples \
   49.80 -  HOL-Statespace \
   49.81 -      TLA-Buffer \
   49.82 -      TLA-Inc \
   49.83 -      TLA-Memory \
   49.84 -  HOL-TPTP \
   49.85 -  HOL-UNITY \
   49.86 -  HOL-Unix \
   49.87 -  HOL-Word-Examples \
   49.88 -  HOL-ZF
   49.89 -    # ^ this is the sort position
   49.90 -
   49.91 -benchmark: \
   49.92 -  HOL-Datatype_Benchmark \
   49.93 -  HOL-Quickcheck_Benchmark \
   49.94 -  HOL-Record_Benchmark
   49.95 -
   49.96 -images-no-smlnj: \
   49.97 -  HOL-Probability
   49.98 -
   49.99 -test-no-smlnj: \
  49.100 -  HOL-ex \
  49.101 -  HOL-Decision_Procs \
  49.102 -  HOL-Proofs-Extraction \
  49.103 -  HOL-Nominal-Examples
  49.104 -
  49.105 -all: test-no-smlnj test images-no-smlnj images
  49.106 -full: all benchmark
  49.107 -smlnj: test images
  49.108 -
  49.109 -
  49.110 -## global settings
  49.111 -
  49.112 -SRC = $(ISABELLE_HOME)/src
  49.113 -OUT = $(ISABELLE_OUTPUT)
  49.114 -LOG = $(OUT)/log
  49.115 -
  49.116 -
  49.117 -## HOL
  49.118 -
  49.119 -HOL: Pure $(OUT)/HOL
  49.120 -
  49.121 -HOL-Base: Pure $(OUT)/HOL-Base
  49.122 -
  49.123 -HOL-Plain: Pure $(OUT)/HOL-Plain
  49.124 -
  49.125 -HOL-Main: Pure $(OUT)/HOL-Main
  49.126 +all:
  49.127 +	@$(ISABELLE_TOOL) build -a
  49.128  
  49.129  Pure:
  49.130 -	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
  49.131 -
  49.132 -$(OUT)/Pure: Pure
  49.133 -
  49.134 -BASE_DEPENDENCIES = $(OUT)/Pure \
  49.135 -  $(SRC)/Provers/blast.ML \
  49.136 -  $(SRC)/Provers/clasimp.ML \
  49.137 -  $(SRC)/Provers/classical.ML \
  49.138 -  $(SRC)/Provers/hypsubst.ML \
  49.139 -  $(SRC)/Provers/quantifier1.ML \
  49.140 -  $(SRC)/Provers/splitter.ML \
  49.141 -  $(SRC)/Tools/Code/code_haskell.ML \
  49.142 -  $(SRC)/Tools/Code/code_ml.ML \
  49.143 -  $(SRC)/Tools/Code/code_namespace.ML \
  49.144 -  $(SRC)/Tools/Code/code_preproc.ML \
  49.145 -  $(SRC)/Tools/Code/code_printer.ML \
  49.146 -  $(SRC)/Tools/Code/code_runtime.ML \
  49.147 -  $(SRC)/Tools/Code/code_scala.ML \
  49.148 -  $(SRC)/Tools/Code/code_simp.ML \
  49.149 -  $(SRC)/Tools/Code/code_target.ML \
  49.150 -  $(SRC)/Tools/Code/code_thingol.ML \
  49.151 -  $(SRC)/Tools/Code_Generator.thy \
  49.152 -  $(SRC)/Tools/IsaPlanner/isand.ML \
  49.153 -  $(SRC)/Tools/IsaPlanner/rw_inst.ML \
  49.154 -  $(SRC)/Tools/IsaPlanner/rw_tools.ML \
  49.155 -  $(SRC)/Tools/IsaPlanner/zipper.ML \
  49.156 -  $(SRC)/Tools/atomize_elim.ML \
  49.157 -  $(SRC)/Tools/cache_io.ML \
  49.158 -  $(SRC)/Tools/case_product.ML \
  49.159 -  $(SRC)/Tools/coherent.ML \
  49.160 -  $(SRC)/Tools/cong_tac.ML \
  49.161 -  $(SRC)/Tools/eqsubst.ML \
  49.162 -  $(SRC)/Tools/induct.ML \
  49.163 -  $(SRC)/Tools/induct_tacs.ML \
  49.164 -  $(SRC)/Tools/induction.ML \
  49.165 -  $(SRC)/Tools/intuitionistic.ML \
  49.166 -  $(SRC)/Tools/misc_legacy.ML \
  49.167 -  $(SRC)/Tools/nbe.ML \
  49.168 -  $(SRC)/Tools/project_rule.ML \
  49.169 -  $(SRC)/Tools/quickcheck.ML \
  49.170 -  $(SRC)/Tools/solve_direct.ML \
  49.171 -  $(SRC)/Tools/subtyping.ML \
  49.172 -  $(SRC)/Tools/try.ML \
  49.173 -  $(SRC)/Tools/value.ML \
  49.174 -  HOL.thy \
  49.175 -  Tools/hologic.ML \
  49.176 -  Tools/simpdata.ML
  49.177 -
  49.178 -$(OUT)/HOL-Base: base.ML $(BASE_DEPENDENCIES)
  49.179 -	@$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base
  49.180 -
  49.181 -PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES) \
  49.182 -  $(SRC)/Provers/Arith/cancel_div_mod.ML \
  49.183 -  $(SRC)/Provers/Arith/fast_lin_arith.ML \
  49.184 -  $(SRC)/Provers/order.ML \
  49.185 -  $(SRC)/Provers/trancl.ML \
  49.186 -  $(SRC)/Tools/Metis/metis.ML \
  49.187 -  $(SRC)/Tools/rat.ML \
  49.188 -  ATP.thy \
  49.189 -  Complete_Lattices.thy \
  49.190 -  Complete_Partial_Order.thy \
  49.191 -  Datatype.thy \
  49.192 -  Extraction.thy \
  49.193 -  Fields.thy \
  49.194 -  Finite_Set.thy \
  49.195 -  Fun.thy \
  49.196 -  FunDef.thy \
  49.197 -  Groups.thy \
  49.198 -  Inductive.thy \
  49.199 -  Lattices.thy \
  49.200 -  Meson.thy \
  49.201 -  Metis.thy \
  49.202 -  Nat.thy \
  49.203 -  Num.thy \
  49.204 -  Option.thy \
  49.205 -  Orderings.thy \
  49.206 -  Partial_Function.thy \
  49.207 -  Plain.thy \
  49.208 -  Power.thy \
  49.209 -  Product_Type.thy \
  49.210 -  Relation.thy \
  49.211 -  Rings.thy \
  49.212 -  SAT.thy \
  49.213 -  Set.thy \
  49.214 -  Sum_Type.thy \
  49.215 -  Tools/ATP/atp_problem.ML \
  49.216 -  Tools/ATP/atp_problem_generate.ML \
  49.217 -  Tools/ATP/atp_proof.ML \
  49.218 -  Tools/ATP/atp_proof_reconstruct.ML \
  49.219 -  Tools/ATP/atp_proof_redirect.ML \
  49.220 -  Tools/ATP/atp_systems.ML \
  49.221 -  Tools/ATP/atp_util.ML \
  49.222 -  Tools/Datatype/datatype.ML \
  49.223 -  Tools/Datatype/datatype_aux.ML \
  49.224 -  Tools/Datatype/datatype_case.ML \
  49.225 -  Tools/Datatype/datatype_codegen.ML \
  49.226 -  Tools/Datatype/datatype_data.ML \
  49.227 -  Tools/Datatype/datatype_prop.ML \
  49.228 -  Tools/Datatype/datatype_realizer.ML \
  49.229 -  Tools/Datatype/primrec.ML \
  49.230 -  Tools/Datatype/rep_datatype.ML \
  49.231 -  Tools/Function/context_tree.ML \
  49.232 -  Tools/Function/fun.ML \
  49.233 -  Tools/Function/function.ML \
  49.234 -  Tools/Function/function_common.ML \
  49.235 -  Tools/Function/function_core.ML \
  49.236 -  Tools/Function/function_lib.ML \
  49.237 -  Tools/Function/induction_schema.ML \
  49.238 -  Tools/Function/lexicographic_order.ML \
  49.239 -  Tools/Function/measure_functions.ML \
  49.240 -  Tools/Function/mutual.ML \
  49.241 -  Tools/Function/partial_function.ML \
  49.242 -  Tools/Function/pat_completeness.ML \
  49.243 -  Tools/Function/pattern_split.ML \
  49.244 -  Tools/Function/relation.ML \
  49.245 -  Tools/Function/scnp_reconstruct.ML \
  49.246 -  Tools/Function/scnp_solve.ML \
  49.247 -  Tools/Function/size.ML \
  49.248 -  Tools/Function/sum_tree.ML \
  49.249 -  Tools/Function/termination.ML \
  49.250 -  Tools/Meson/meson.ML \
  49.251 -  Tools/Meson/meson_clausify.ML \
  49.252 -  Tools/Meson/meson_tactic.ML \
  49.253 -  Tools/Metis/metis_generate.ML \
  49.254 -  Tools/Metis/metis_reconstruct.ML \
  49.255 -  Tools/Metis/metis_tactic.ML \
  49.256 -  Tools/arith_data.ML \
  49.257 -  Tools/cnf_funcs.ML \
  49.258 -  Tools/enriched_type.ML \
  49.259 -  Tools/group_cancel.ML \
  49.260 -  Tools/inductive.ML \
  49.261 -  Tools/inductive_realizer.ML \
  49.262 -  Tools/inductive_set.ML \
  49.263 -  Tools/lambda_lifting.ML \
  49.264 -  Tools/lin_arith.ML \
  49.265 -  Tools/monomorph.ML \
  49.266 -  Tools/nat_arith.ML \
  49.267 -  Tools/prop_logic.ML \
  49.268 -  Tools/refute.ML \
  49.269 -  Tools/rewrite_hol_proof.ML \
  49.270 -  Tools/sat_funcs.ML \
  49.271 -  Tools/sat_solver.ML \
  49.272 -  Tools/set_comprehension_pointfree.ML \
  49.273 -  Tools/split_rule.ML \
  49.274 -  Tools/try0.ML \
  49.275 -  Tools/typedef.ML \
  49.276 -  Transitive_Closure.thy \
  49.277 -  Typedef.thy \
  49.278 -  Wellfounded.thy
  49.279 -
  49.280 -$(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES)
  49.281 -	@$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
  49.282 +	@$(ISABELLE_TOOL) build -b Pure
  49.283  
  49.284 -MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
  49.285 -  Big_Operators.thy \
  49.286 -  Code_Evaluation.thy \
  49.287 -  Code_Numeral.thy \
  49.288 -  Divides.thy \
  49.289 -  DSequence.thy \
  49.290 -  Equiv_Relations.thy \
  49.291 -  Enum.thy \
  49.292 -  Groebner_Basis.thy \
  49.293 -  Hilbert_Choice.thy \
  49.294 -  Int.thy \
  49.295 -  Lazy_Sequence.thy \
  49.296 -  Lifting.thy \
  49.297 -  List.thy \
  49.298 -  Main.thy \
  49.299 -  Map.thy \
  49.300 -  Nat_Transfer.thy \
  49.301 -  New_DSequence.thy \
  49.302 -  New_Random_Sequence.thy \
  49.303 -  Nitpick.thy \
  49.304 -  Numeral_Simprocs.thy \
  49.305 -  Presburger.thy \
  49.306 -  Predicate.thy \
  49.307 -  Predicate_Compile.thy \
  49.308 -  Quickcheck.thy \
  49.309 -  Quickcheck_Exhaustive.thy \
  49.310 -  Quickcheck_Narrowing.thy \
  49.311 -  Quotient.thy \
  49.312 -  Random.thy \
  49.313 -  Random_Sequence.thy \
  49.314 -  Record.thy \
  49.315 -  Refute.thy \
  49.316 -  Semiring_Normalization.thy \
  49.317 -  Set_Interval.thy \
  49.318 -  Sledgehammer.thy \
  49.319 -  SMT.thy \
  49.320 -  String.thy \
  49.321 -  Transfer.thy \
  49.322 -  Typerep.thy \
  49.323 -  $(SRC)/Provers/Arith/assoc_fold.ML \
  49.324 -  $(SRC)/Provers/Arith/cancel_numeral_factor.ML \
  49.325 -  $(SRC)/Provers/Arith/cancel_numerals.ML \
  49.326 -  $(SRC)/Provers/Arith/combine_numerals.ML \
  49.327 -  $(SRC)/Provers/Arith/extract_common_term.ML \
  49.328 -  Tools/choice_specification.ML \
  49.329 -  Tools/code_evaluation.ML \
  49.330 -  Tools/groebner.ML \
  49.331 -  Tools/int_arith.ML \
  49.332 -  Tools/legacy_transfer.ML \
  49.333 -  Tools/Lifting/lifting_def.ML \
  49.334 -  Tools/Lifting/lifting_info.ML \
  49.335 -  Tools/Lifting/lifting_term.ML \
  49.336 -  Tools/Lifting/lifting_setup.ML \
  49.337 -  Tools/list_code.ML \
  49.338 -  Tools/list_to_set_comprehension.ML \
  49.339 -  Tools/nat_numeral_simprocs.ML \
  49.340 -  Tools/Nitpick/kodkod.ML \
  49.341 -  Tools/Nitpick/kodkod_sat.ML \
  49.342 -  Tools/Nitpick/nitpick.ML \
  49.343 -  Tools/Nitpick/nitpick_hol.ML \
  49.344 -  Tools/Nitpick/nitpick_isar.ML \
  49.345 -  Tools/Nitpick/nitpick_kodkod.ML \
  49.346 -  Tools/Nitpick/nitpick_model.ML \
  49.347 -  Tools/Nitpick/nitpick_mono.ML \
  49.348 -  Tools/Nitpick/nitpick_nut.ML \
  49.349 -  Tools/Nitpick/nitpick_peephole.ML \
  49.350 -  Tools/Nitpick/nitpick_preproc.ML \
  49.351 -  Tools/Nitpick/nitpick_rep.ML \
  49.352 -  Tools/Nitpick/nitpick_scope.ML \
  49.353 -  Tools/Nitpick/nitpick_tests.ML \
  49.354 -  Tools/Nitpick/nitpick_util.ML \
  49.355 -  Tools/numeral.ML \
  49.356 -  Tools/numeral_simprocs.ML \
  49.357 -  Tools/Predicate_Compile/core_data.ML \
  49.358 -  Tools/Predicate_Compile/mode_inference.ML \
  49.359 -  Tools/Predicate_Compile/predicate_compile_aux.ML \
  49.360 -  Tools/Predicate_Compile/predicate_compile_compilations.ML \
  49.361 -  Tools/Predicate_Compile/predicate_compile_core.ML \
  49.362 -  Tools/Predicate_Compile/predicate_compile_data.ML \
  49.363 -  Tools/Predicate_Compile/predicate_compile_fun.ML \
  49.364 -  Tools/Predicate_Compile/predicate_compile.ML \
  49.365 -  Tools/Predicate_Compile/predicate_compile_proof.ML \
  49.366 -  Tools/Predicate_Compile/predicate_compile_specialisation.ML \
  49.367 -  Tools/Predicate_Compile/predicate_compile_pred.ML \
  49.368 -  Tools/Qelim/cooper.ML \
  49.369 -  Tools/Qelim/cooper_procedure.ML \
  49.370 -  Tools/Qelim/qelim.ML \
  49.371 -  Tools/Quickcheck/exhaustive_generators.ML \
  49.372 -  Tools/Quickcheck/random_generators.ML \
  49.373 -  Tools/Quickcheck/quickcheck_common.ML \
  49.374 -  Tools/Quickcheck/narrowing_generators.ML \
  49.375 -  Tools/Quickcheck/Narrowing_Engine.hs \
  49.376 -  Tools/Quickcheck/PNF_Narrowing_Engine.hs \
  49.377 -  Tools/Quotient/quotient_def.ML \
  49.378 -  Tools/Quotient/quotient_info.ML \
  49.379 -  Tools/Quotient/quotient_tacs.ML \
  49.380 -  Tools/Quotient/quotient_term.ML \
  49.381 -  Tools/Quotient/quotient_type.ML \
  49.382 -  Tools/record.ML \
  49.383 -  Tools/semiring_normalizer.ML \
  49.384 -  Tools/Sledgehammer/async_manager.ML \
  49.385 -  Tools/Sledgehammer/sledgehammer_fact.ML \
  49.386 -  Tools/Sledgehammer/sledgehammer_mash.ML \
  49.387 -  Tools/Sledgehammer/sledgehammer_mepo.ML \
  49.388 -  Tools/Sledgehammer/sledgehammer_minimize.ML \
  49.389 -  Tools/Sledgehammer/sledgehammer_isar.ML \
  49.390 -  Tools/Sledgehammer/sledgehammer_provers.ML \
  49.391 -  Tools/Sledgehammer/sledgehammer_run.ML \
  49.392 -  Tools/Sledgehammer/sledgehammer_util.ML \
  49.393 -  Tools/SMT/smtlib_interface.ML \
  49.394 -  Tools/SMT/smt_builtin.ML \
  49.395 -  Tools/SMT/smt_config.ML \
  49.396 -  Tools/SMT/smt_datatypes.ML \
  49.397 -  Tools/SMT/smt_failure.ML \
  49.398 -  Tools/SMT/smt_normalize.ML \
  49.399 -  Tools/SMT/smt_setup_solvers.ML \
  49.400 -  Tools/SMT/smt_solver.ML \
  49.401 -  Tools/SMT/smt_translate.ML \
  49.402 -  Tools/SMT/smt_utils.ML \
  49.403 -  Tools/SMT/z3_interface.ML \
  49.404 -  Tools/SMT/z3_model.ML \
  49.405 -  Tools/SMT/z3_proof_literals.ML \
  49.406 -  Tools/SMT/z3_proof_methods.ML \
  49.407 -  Tools/SMT/z3_proof_parser.ML \
  49.408 -  Tools/SMT/z3_proof_reconstruction.ML \
  49.409 -  Tools/SMT/z3_proof_tools.ML \
  49.410 -  Tools/string_code.ML \
  49.411 -  Tools/string_syntax.ML \
  49.412 -  Tools/transfer.ML \
  49.413 -
  49.414 -$(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES)
  49.415 -	@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
  49.416 -
  49.417 -HOL_DEPENDENCIES = $(MAIN_DEPENDENCIES) \
  49.418 -  Archimedean_Field.thy \
  49.419 -  Complex.thy \
  49.420 -  Complex_Main.thy \
  49.421 -  Deriv.thy \
  49.422 -  Fact.thy \
  49.423 -  GCD.thy \
  49.424 -  Lim.thy \
  49.425 -  Limits.thy \
  49.426 -  Ln.thy \
  49.427 -  Log.thy \
  49.428 -  Lubs.thy \
  49.429 -  MacLaurin.thy \
  49.430 -  NthRoot.thy \
  49.431 -  Parity.thy \
  49.432 -  RComplete.thy \
  49.433 -  Rat.thy \
  49.434 -  Real.thy \
  49.435 -  RealDef.thy \
  49.436 -  RealVector.thy \
  49.437 -  SEQ.thy \
  49.438 -  Series.thy \
  49.439 -  SupInf.thy \
  49.440 -  Taylor.thy \
  49.441 -  Tools/SMT/smt_real.ML \
  49.442 -  Tools/float_syntax.ML \
  49.443 -  Transcendental.thy
  49.444 -
  49.445 -$(OUT)/HOL: ROOT.ML $(HOL_DEPENDENCIES)
  49.446 -	@$(ISABELLE_TOOL) usedir -b -g true $(OUT)/Pure HOL
  49.447 -
  49.448 -
  49.449 -## HOL-Library
  49.450 -
  49.451 -HOL-Library: HOL $(OUT)/HOL-Library
  49.452 -
  49.453 -$(OUT)/HOL-Library: $(OUT)/HOL Library/ROOT.ML				\
  49.454 -  $(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML			\
  49.455 -  Library/Abstract_Rat.thy $(SRC)/Tools/Adhoc_Overloading.thy		\
  49.456 -  Library/AList.thy Library/AList_Mapping.thy 				\
  49.457 -  Library/BigO.thy Library/Binomial.thy 				\
  49.458 -  Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy	\
  49.459 -  Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy	\
  49.460 -  Library/Code_Char_ord.thy Library/Code_Integer.thy			\
  49.461 -  Library/Code_Nat.thy Library/Code_Natural.thy				\
  49.462 -  Library/Efficient_Nat.thy Library/Code_Prolog.thy			\
  49.463 -  Library/Code_Real_Approx_By_Float.thy					\
  49.464 -  Tools/Predicate_Compile/code_prolog.ML Library/ContNotDenum.thy	\
  49.465 -  Library/Continuity.thy						\
  49.466 -  Library/Convex.thy Library/Countable.thy				\
  49.467 -  Library/Debug.thy							\
  49.468 -  Library/Dlist.thy Library/Eval_Witness.thy				\
  49.469 -  Library/DAList.thy Library/Dlist.thy					\
  49.470 -  Library/Eval_Witness.thy						\
  49.471 -  Library/Extended_Real.thy Library/Extended_Nat.thy			\
  49.472 -  Library/FinFun.thy Library/FinFun_Syntax.thy Library/Float.thy	\
  49.473 -  Library/Formal_Power_Series.thy Library/Fraction_Field.thy		\
  49.474 -  Library/FrechetDeriv.thy Library/FuncSet.thy				\
  49.475 -  Library/Function_Algebras.thy Library/Function_Division.thy		\
  49.476 -  Library/Fundamental_Theorem_Algebra.thy				\
  49.477 -  Library/Glbs.thy Library/Indicator_Function.thy			\
  49.478 -  Library/Infinite_Set.thy Library/Inner_Product.thy			\
  49.479 -  Library/Kleene_Algebra.thy Library/LaTeXsugar.thy			\
  49.480 -  Library/Lattice_Algebras.thy Library/Lattice_Syntax.thy		\
  49.481 -  Library/Library.thy Library/List_Prefix.thy				\
  49.482 -  Library/List_lexord.thy Library/Mapping.thy Library/Monad_Syntax.thy	\
  49.483 -  Library/Multiset.thy Library/Nat_Bijection.thy			\
  49.484 -  Library/Numeral_Type.thy Library/Old_Recdef.thy			\
  49.485 -  Library/OptionalSugar.thy Library/Order_Relation.thy			\
  49.486 -  Library/Parallel.thy							\
  49.487 -  Library/Permutation.thy Library/Permutations.thy			\
  49.488 -  Library/Phantom_Type.thy Library/Poly_Deriv.thy			\
  49.489 -  Library/Polynomial.thy Library/Predicate_Compile_Quickcheck.thy	\
  49.490 -  Library/Preorder.thy Library/Product_Vector.thy			\
  49.491 -  Library/Product_ord.thy Library/Product_plus.thy 			\
  49.492 -  Library/Product_Lattice.thy Library/Quickcheck_Types.thy 		\
  49.493 -  Library/Quotient_List.thy Library/Quotient_Option.thy 		\
  49.494 -  Library/Quotient_Product.thy Library/Quotient_Set.thy 		\
  49.495 -  Library/Quotient_Sum.thy Library/Quotient_Syntax.thy 			\
  49.496 -  Library/Quotient_Type.thy Library/RBT.thy Library/RBT_Impl.thy	\
  49.497 -  Library/RBT_Mapping.thy Library/README.html Library/Saturated.thy	\
  49.498 -  Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy	\
  49.499 -  Library/Reflection.thy Library/Sublist_Order.thy			\
  49.500 -  Library/Sum_of_Squares.thy Library/Sum_of_Squares/sos_wrapper.ML	\
  49.501 -  Library/Sum_of_Squares/sum_of_squares.ML Library/Target_Numeral.thy	\
  49.502 -  Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy		\
  49.503 -  Library/Wfrec.thy Library/While_Combinator.thy Library/Zorn.thy	\
  49.504 -  $(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML	\
  49.505 -  Library/reflection.ML Library/reify_data.ML				\
  49.506 -  Library/document/root.bib Library/document/root.tex			\
  49.507 -  Tools/TFL/casesplit.ML Tools/TFL/dcterm.ML Tools/TFL/post.ML		\
  49.508 -  Tools/TFL/rules.ML Tools/TFL/tfl.ML Tools/TFL/thms.ML			\
  49.509 -  Tools/TFL/thry.ML Tools/TFL/usyntax.ML Tools/TFL/utils.ML		\
  49.510 -  Tools/recdef.ML
  49.511 -	@cd Library; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL-Library
  49.512 -
  49.513 -
  49.514 -## HOL-Hahn_Banach
  49.515 -
  49.516 -HOL-Hahn_Banach: HOL $(LOG)/HOL-Hahn_Banach.gz
  49.517 -
  49.518 -$(LOG)/HOL-Hahn_Banach.gz: $(OUT)/HOL Hahn_Banach/Bounds.thy		\
  49.519 -  Hahn_Banach/Function_Norm.thy Hahn_Banach/Function_Order.thy		\
  49.520 -  Hahn_Banach/Hahn_Banach.thy Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	\
  49.521 -  Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Hahn_Banach/Linearform.thy	\
  49.522 -  Hahn_Banach/Normed_Space.thy Hahn_Banach/README.html			\
  49.523 -  Hahn_Banach/ROOT.ML Hahn_Banach/Subspace.thy				\
  49.524 -  Hahn_Banach/Vector_Space.thy Hahn_Banach/Zorn_Lemma.thy		\
  49.525 -  Hahn_Banach/document/root.bib Hahn_Banach/document/root.tex
  49.526 -	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hahn_Banach
  49.527 -
  49.528 -
  49.529 -## HOL-Induct
  49.530 -
  49.531 -HOL-Induct: HOL $(LOG)/HOL-Induct.gz
  49.532 -
  49.533 -$(LOG)/HOL-Induct.gz: $(OUT)/HOL Induct/Com.thy Induct/Comb.thy		\
  49.534 -  Induct/Ordinals.thy Induct/PropLog.thy Induct/QuoNestedDataType.thy	\
  49.535 -  Induct/QuoDataType.thy Induct/ROOT.ML Induct/Sexp.thy			\
  49.536 -  Induct/Sigma_Algebra.thy Induct/ABexp.thy Induct/SList.thy		\
  49.537 -  Induct/Term.thy Induct/Tree.thy Induct/document/root.tex
  49.538 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Induct
  49.539 -
  49.540 -
  49.541 -## HOL-IMP
  49.542 -
  49.543 -HOL-IMP: HOL $(OUT)/HOL-IMP
  49.544 +HOL:
  49.545 +	@$(ISABELLE_TOOL) build -b HOL
  49.546  
  49.547 -$(OUT)/HOL-IMP: $(OUT)/HOL \
  49.548 -  IMP/ACom.thy \
  49.549 -  IMP/Abs_Int0.thy IMP/Abs_State.thy IMP/Abs_Int1.thy \
  49.550 -  IMP/Abs_Int1_const.thy IMP/Abs_Int1_parity.thy \
  49.551 -  IMP/Abs_Int2.thy IMP/Abs_Int2_ivl.thy IMP/Abs_Int3.thy \
  49.552 -  IMP/Abs_Int_ITP/Abs_Int0_ITP.thy IMP/Abs_Int_ITP/Abs_State_ITP.thy \
  49.553 -  IMP/Abs_Int_ITP/Abs_Int1_ITP.thy IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy \
  49.554 -  IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy IMP/Abs_Int_ITP/Abs_Int2_ITP.thy \
  49.555 -  IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy IMP/Abs_Int_ITP/Abs_Int3_ITP.thy \
  49.556 -  IMP/Abs_Int_Den/Abs_Int_den0_fun.thy \
  49.557 -  IMP/Abs_Int_Den/Abs_State_den.thy  IMP/Abs_Int_Den/Abs_Int_den0.thy \
  49.558 -  IMP/Abs_Int_Den/Abs_Int_den0_const.thy IMP/Abs_Int_Den/Abs_Int_den1.thy \
  49.559 -  IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy IMP/Abs_Int_Den/Abs_Int_den2.thy \
  49.560 -  IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy	IMP/Big_Step.thy IMP/C_like.thy \
  49.561 -  IMP/Collecting.thy IMP/Collecting_list.thy IMP/Collecting1.thy IMP/Com.thy \
  49.562 -  IMP/Compiler.thy IMP/Comp_Rev.thy \
  49.563 -  IMP/Def_Ass.thy IMP/Def_Ass_Big.thy IMP/Def_Ass_Exp.thy \
  49.564 -  IMP/Def_Ass_Small.thy IMP/Def_Ass_Sound_Big.thy \
  49.565 -  IMP/Def_Ass_Sound_Small.thy IMP/Denotation.thy IMP/Hoare.thy \
  49.566 -  IMP/HoareT.thy IMP/Hoare_Examples.thy IMP/Hoare_Sound_Complete.thy \
  49.567 -  IMP/Live.thy IMP/Live_True.thy IMP/OO.thy IMP/Poly_Types.thy IMP/Procs.thy \
  49.568 -  IMP/Procs_Dyn_Vars_Dyn.thy IMP/Procs_Stat_Vars_Dyn.thy \
  49.569 -  IMP/Procs_Stat_Vars_Stat.thy IMP/Sec_Type_Expr.thy IMP/Sec_Typing.thy \
  49.570 -  IMP/Sec_TypingT.thy IMP/Small_Step.thy IMP/Star.thy IMP/Types.thy \
  49.571 -  IMP/VC.thy IMP/Vars.thy \
  49.572 -  IMP/ROOT.ML IMP/document/root.tex IMP/document/root.bib
  49.573 -	@cd IMP && $(ISABELLE_TOOL) usedir -g true -b $(OUT)/HOL HOL-IMP
  49.574 -
  49.575 -## HOL-IMPP
  49.576 -
  49.577 -HOL-IMPP: HOL $(LOG)/HOL-IMPP.gz
  49.578 -
  49.579 -$(LOG)/HOL-IMPP.gz: $(OUT)/HOL IMPP/ROOT.ML IMPP/Com.thy		\
  49.580 -  IMPP/Natural.thy IMPP/Hoare.thy IMPP/Misc.thy IMPP/EvenOdd.thy
  49.581 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL IMPP
  49.582 -
  49.583 -
  49.584 -## HOL-Import
  49.585 -
  49.586 -HOL-Import: $(LOG)/HOL-Import.gz
  49.587 -
  49.588 -$(LOG)/HOL-Import.gz: $(OUT)/HOL \
  49.589 -  Import/ROOT.ML \
  49.590 -  Import/Import_Setup.thy \
  49.591 -  Import/import_data.ML \
  49.592 -  Import/import_rule.ML \
  49.593 -  Import/HOL_Light_Maps.thy \
  49.594 -  Import/HOL_Light_Import.thy
  49.595 -	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Import
  49.596 -
  49.597 -
  49.598 -## HOL-Number_Theory
  49.599 -
  49.600 -HOL-Number_Theory: HOL $(LOG)/HOL-Number_Theory.gz
  49.601 -
  49.602 -$(LOG)/HOL-Number_Theory.gz: $(OUT)/HOL $(ALGEBRA_DEPENDENCIES) \
  49.603 -  Library/Multiset.thy \
  49.604 -  Number_Theory/Binomial.thy \
  49.605 -  Number_Theory/Cong.thy \
  49.606 -  Number_Theory/Fib.thy \
  49.607 -  Number_Theory/MiscAlgebra.thy \
  49.608 -  Number_Theory/Number_Theory.thy \
  49.609 -  Number_Theory/Residues.thy \
  49.610 -  Number_Theory/UniqueFactorization.thy  \
  49.611 -  Number_Theory/ROOT.ML
  49.612 -	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Number_Theory
  49.613 -
  49.614 -
  49.615 -## HOL-Old_Number_Theory
  49.616 -
  49.617 -HOL-Old_Number_Theory: HOL $(LOG)/HOL-Old_Number_Theory.gz
  49.618 -
  49.619 -$(LOG)/HOL-Old_Number_Theory.gz: $(OUT)/HOL Library/Permutation.thy	\
  49.620 -  Old_Number_Theory/Primes.thy Old_Number_Theory/Fib.thy		\
  49.621 -  Old_Number_Theory/Factorization.thy Old_Number_Theory/BijectionRel.thy\
  49.622 -  Old_Number_Theory/Chinese.thy Old_Number_Theory/EulerFermat.thy	\
  49.623 -  Old_Number_Theory/IntFact.thy Old_Number_Theory/IntPrimes.thy		\
  49.624 -  Old_Number_Theory/WilsonBij.thy Old_Number_Theory/WilsonRuss.thy	\
  49.625 -  Old_Number_Theory/Finite2.thy Old_Number_Theory/Int2.thy		\
  49.626 -  Old_Number_Theory/EvenOdd.thy Old_Number_Theory/Residues.thy		\
  49.627 -  Old_Number_Theory/Euler.thy Old_Number_Theory/Gauss.thy		\
  49.628 -  Old_Number_Theory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy	\
  49.629 -  Old_Number_Theory/Legacy_GCD.thy Old_Number_Theory/Pocklington.thy	\
  49.630 -  Old_Number_Theory/ROOT.ML
  49.631 -	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Old_Number_Theory
  49.632 -
  49.633 -
  49.634 -## HOL-Hoare
  49.635 -
  49.636 -HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz
  49.637 -
  49.638 -$(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.thy Hoare/Examples.thy	\
  49.639 -  Hoare/Hoare.thy Hoare/hoare_syntax.ML Hoare/hoare_tac.ML		\
  49.640 -  Hoare/Heap.thy Hoare/Hoare_Logic.thy Hoare/Hoare_Logic_Abort.thy	\
  49.641 -  Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy Hoare/ROOT.ML		\
  49.642 -  Hoare/ExamplesAbort.thy Hoare/HeapSyntaxAbort.thy			\
  49.643 -  Hoare/SchorrWaite.thy Hoare/Separation.thy Hoare/SepLogHeap.thy	\
  49.644 -  Hoare/document/root.tex Hoare/document/root.bib
  49.645 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Hoare
  49.646 -
  49.647 -
  49.648 -## HOL-Hoare_Parallel
  49.649 -
  49.650 -HOL-Hoare_Parallel: HOL $(LOG)/HOL-Hoare_Parallel.gz
  49.651 -
  49.652 -$(LOG)/HOL-Hoare_Parallel.gz: $(OUT)/HOL Hoare_Parallel/Gar_Coll.thy	\
  49.653 -  Hoare_Parallel/Graph.thy Hoare_Parallel/Hoare_Parallel.thy		\
  49.654 -  Hoare_Parallel/Mul_Gar_Coll.thy Hoare_Parallel/OG_Com.thy		\
  49.655 -  Hoare_Parallel/OG_Examples.thy Hoare_Parallel/OG_Hoare.thy		\
  49.656 -  Hoare_Parallel/OG_Syntax.thy Hoare_Parallel/OG_Tactics.thy		\
  49.657 -  Hoare_Parallel/OG_Tran.thy Hoare_Parallel/Quote_Antiquote.thy		\
  49.658 -  Hoare_Parallel/RG_Com.thy Hoare_Parallel/RG_Examples.thy		\
  49.659 -  Hoare_Parallel/RG_Hoare.thy Hoare_Parallel/RG_Syntax.thy		\
  49.660 -  Hoare_Parallel/RG_Tran.thy Hoare_Parallel/ROOT.ML			\
  49.661 -  Hoare_Parallel/document/root.tex Hoare_Parallel/document/root.bib
  49.662 -	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hoare_Parallel
  49.663 -
  49.664 -
  49.665 -## HOL-Library-Codegenerator_Test
  49.666 -
  49.667 -HOL-Library-Codegenerator_Test: HOL-Library $(LOG)/HOL-Library-Codegenerator_Test.gz
  49.668 -
  49.669 -$(LOG)/HOL-Library-Codegenerator_Test.gz: $(OUT)/HOL-Library \
  49.670 -  Codegenerator_Test/ROOT.ML \
  49.671 -  Codegenerator_Test/Candidates.thy \
  49.672 -  Codegenerator_Test/Candidates_Pretty.thy \
  49.673 -  Codegenerator_Test/Generate.thy \
  49.674 -  Codegenerator_Test/Generate_Pretty.thy
  49.675 -	@$(ISABELLE_TOOL) usedir -d false -g false -i false $(OUT)/HOL-Library Codegenerator_Test
  49.676 -
  49.677 -
  49.678 -## HOL-Metis_Examples
  49.679 -
  49.680 -HOL-Metis_Examples: HOL $(LOG)/HOL-Metis_Examples.gz
  49.681 -
  49.682 -$(LOG)/HOL-Metis_Examples.gz: $(OUT)/HOL Metis_Examples/ROOT.ML \
  49.683 -  Metis_Examples/Abstraction.thy Metis_Examples/Big_O.thy \
  49.684 -  Metis_Examples/Binary_Tree.thy Metis_Examples/Clausification.thy \
  49.685 -  Metis_Examples/Message.thy Metis_Examples/Proxies.thy \
  49.686 -  Metis_Examples/Sets.thy Metis_Examples/Tarski.thy \
  49.687 -  Metis_Examples/Trans_Closure.thy Metis_Examples/Type_Encodings.thy
  49.688 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Metis_Examples
  49.689 -
  49.690 -
  49.691 -## HOL-Nitpick_Examples
  49.692 -
  49.693 -HOL-Nitpick_Examples: HOL $(LOG)/HOL-Nitpick_Examples.gz
  49.694 -
  49.695 -$(LOG)/HOL-Nitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML \
  49.696 -  Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy \
  49.697 -  Nitpick_Examples/Hotel_Nits.thy Nitpick_Examples/Induct_Nits.thy \
  49.698 -  Nitpick_Examples/Integer_Nits.thy Nitpick_Examples/Manual_Nits.thy \
  49.699 -  Nitpick_Examples/Mini_Nits.thy Nitpick_Examples/Mono_Nits.thy \
  49.700 -  Nitpick_Examples/Nitpick_Examples.thy Nitpick_Examples/Pattern_Nits.thy \
  49.701 -  Nitpick_Examples/Record_Nits.thy Nitpick_Examples/Refute_Nits.thy \
  49.702 -  Nitpick_Examples/Special_Nits.thy Nitpick_Examples/Tests_Nits.thy \
  49.703 -  Nitpick_Examples/Typedef_Nits.thy Nitpick_Examples/minipick.ML
  49.704 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Nitpick_Examples
  49.705 -
  49.706 -
  49.707 -## HOL-Algebra
  49.708 -
  49.709 -HOL-Algebra: HOL $(OUT)/HOL-Algebra
  49.710 -
  49.711 -ALGEBRA_DEPENDENCIES = $(OUT)/HOL \
  49.712 -  Algebra/ROOT.ML \
  49.713 -  Library/Binomial.thy \
  49.714 -  Library/FuncSet.thy \
  49.715 -  Library/Multiset.thy \
  49.716 -  Library/Permutation.thy \
  49.717 -  Number_Theory/Primes.thy \
  49.718 -  Algebra/AbelCoset.thy \
  49.719 -  Algebra/Bij.thy \
  49.720 -  Algebra/Congruence.thy \
  49.721 -  Algebra/Coset.thy \
  49.722 -  Algebra/Divisibility.thy \
  49.723 -  Algebra/Exponent.thy \
  49.724 -  Algebra/FiniteProduct.thy \
  49.725 -  Algebra/Group.thy \
  49.726 -  Algebra/Ideal.thy \
  49.727 -  Algebra/IntRing.thy \
  49.728 -  Algebra/Lattice.thy \
  49.729 -  Algebra/Module.thy \
  49.730 -  Algebra/QuotRing.thy \
  49.731 -  Algebra/Ring.thy \
  49.732 -  Algebra/RingHom.thy \
  49.733 -  Algebra/Sylow.thy \
  49.734 -  Algebra/UnivPoly.thy \
  49.735 -  Algebra/abstract/Abstract.thy \
  49.736 -  Algebra/abstract/Factor.thy \
  49.737 -  Algebra/abstract/Field.thy \
  49.738 -  Algebra/abstract/Ideal2.thy \
  49.739 -  Algebra/abstract/PID.thy \
  49.740 -  Algebra/abstract/Ring2.thy \
  49.741 -  Algebra/abstract/RingHomo.thy \
  49.742 -  Algebra/document/root.tex \
  49.743 -  Algebra/document/root.tex \
  49.744 -  Algebra/poly/LongDiv.thy \
  49.745 -  Algebra/poly/PolyHomo.thy \
  49.746 -  Algebra/poly/Polynomial.thy \
  49.747 -  Algebra/poly/UnivPoly2.thy \
  49.748 -  Algebra/ringsimp.ML
  49.749 -
  49.750 -$(OUT)/HOL-Algebra: $(ALGEBRA_DEPENDENCIES)
  49.751 -	@cd Algebra; $(ISABELLE_TOOL) usedir -b -g true -V outline=/proof,/ML $(OUT)/HOL HOL-Algebra
  49.752 -
  49.753 -
  49.754 -## HOL-Auth
  49.755 -
  49.756 -HOL-Auth: HOL $(LOG)/HOL-Auth.gz
  49.757 -
  49.758 -$(LOG)/HOL-Auth.gz: $(OUT)/HOL 						\
  49.759 -  Auth/Auth_Shared.thy Auth/Auth_Public.thy Auth/All_Symmetric.thy	\
  49.760 -  Auth/Guard/Auth_Guard_Shared.thy					\
  49.761 -  Auth/Guard/Auth_Guard_Public.thy					\
  49.762 -  Auth/Smartcard/Auth_Smartcard.thy Auth/All_Symmetric.thy		\
  49.763 -  Auth/CertifiedEmail.thy Auth/Event.thy Auth/Message.thy		\
  49.764 -  Auth/NS_Public.thy Auth/NS_Public_Bad.thy Auth/NS_Shared.thy		\
  49.765 -  Auth/OtwayRees.thy Auth/OtwayReesBella.thy Auth/OtwayRees_AN.thy	\
  49.766 -  Auth/OtwayRees_Bad.thy Auth/Public.thy Auth/ROOT.ML Auth/Recur.thy	\
  49.767 -  Auth/Shared.thy Auth/TLS.thy Auth/WooLam.thy Auth/Kerberos_BAN.thy	\
  49.768 -  Auth/Kerberos_BAN_Gets.thy Auth/KerberosIV.thy			\
  49.769 -  Auth/KerberosIV_Gets.thy Auth/KerberosV.thy Auth/Yahalom.thy		\
  49.770 -  Auth/Yahalom2.thy Auth/Yahalom_Bad.thy Auth/ZhouGollmann.thy		\
  49.771 -  Auth/Guard/Analz.thy Auth/Guard/Extensions.thy Auth/Guard/GuardK.thy	\
  49.772 -  Auth/Guard/Guard_Public.thy Auth/Guard/Guard_Shared.thy		\
  49.773 -  Auth/Guard/Guard.thy Auth/Guard/List_Msg.thy				\
  49.774 -  Auth/Guard/Guard_NS_Public.thy Auth/Guard/Guard_OtwayRees.thy		\
  49.775 -  Auth/Guard/P1.thy Auth/Guard/P2.thy Auth/Guard/Proto.thy		\
  49.776 -  Auth/Guard/Guard_Yahalom.thy Auth/Smartcard/EventSC.thy		\
  49.777 -  Auth/Smartcard/ShoupRubinBella.thy Auth/Smartcard/ShoupRubin.thy	\
  49.778 -  Auth/Smartcard/Smartcard.thy Auth/document/root.tex
  49.779 -	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Auth
  49.780 +HOL-Library:
  49.781 +	@$(ISABELLE_TOOL) build -b HOL-Library
  49.782  
  49.783 -
  49.784 -## HOL-UNITY
  49.785 -
  49.786 -HOL-UNITY: HOL $(LOG)/HOL-UNITY.gz
  49.787 -
  49.788 -$(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML	\
  49.789 -  UNITY/UNITY_Main.thy UNITY/UNITY_tactics.ML UNITY/Comp.thy		\
  49.790 -  UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy			\
  49.791 -  UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy UNITY/Guar.thy	\
  49.792 -  UNITY/Lift_prog.thy UNITY/ListOrder.thy UNITY/ProgressSets.thy	\
  49.793 -  UNITY/PPROD.thy UNITY/Project.thy UNITY/Rename.thy			\
  49.794 -  UNITY/Transformers.thy UNITY/SubstAx.thy UNITY/UNITY.thy		\
  49.795 -  UNITY/Union.thy UNITY/WFair.thy UNITY/Simple/Channel.thy		\
  49.796 -  UNITY/Simple/Common.thy UNITY/Simple/Deadlock.thy			\
  49.797 -  UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy				\
  49.798 -  UNITY/Simple/NSP_Bad.thy UNITY/Simple/Network.thy			\
  49.799 -  UNITY/Simple/Reach.thy UNITY/Simple/Reachability.thy			\
  49.800 -  UNITY/Simple/Token.thy UNITY/Comp/Alloc.thy UNITY/Comp/AllocBase.thy	\
  49.801 -  UNITY/Comp/AllocImpl.thy UNITY/Comp/Client.thy			\
  49.802 -  UNITY/Comp/Counter.thy UNITY/Comp/Counterc.thy			\
  49.803 -  UNITY/Comp/Handshake.thy UNITY/Comp/PriorityAux.thy			\
  49.804 -  UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy			\
  49.805 -  UNITY/Comp/TimerArray.thy UNITY/document/root.tex
  49.806 -	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL UNITY
  49.807 -
  49.808 -
  49.809 -## HOL-Unix
  49.810 -
  49.811 -HOL-Unix: HOL $(LOG)/HOL-Unix.gz
  49.812 -
  49.813 -$(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/List_Prefix.thy Unix/ROOT.ML	\
  49.814 -  Unix/Nested_Environment.thy Unix/Unix.thy Unix/document/root.bib	\
  49.815 -  Unix/document/root.tex
  49.816 -	@$(ISABELLE_TOOL) usedir -m no_brackets -m no_type_brackets $(OUT)/HOL Unix
  49.817 -
  49.818 -
  49.819 -## HOL-ZF
  49.820 -
  49.821 -HOL-ZF: HOL $(LOG)/HOL-ZF.gz
  49.822 -
  49.823 -$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/LProd.thy \
  49.824 -  ZF/HOLZF.thy ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex
  49.825 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ZF
  49.826 -
  49.827 -
  49.828 -## HOL-Imperative_HOL
  49.829 -
  49.830 -HOL-Imperative_HOL: HOL $(LOG)/HOL-Imperative_HOL.gz
  49.831 -
  49.832 -$(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL \
  49.833 -  Library/Code_Integer.thy \
  49.834 -  Library/Code_Nat.thy \
  49.835 -  Library/Code_Natural.thy \
  49.836 -  Library/Efficient_Nat.thy \
  49.837 -  Imperative_HOL/Array.thy \
  49.838 -  Imperative_HOL/Heap.thy \
  49.839 -  Imperative_HOL/Heap_Monad.thy \
  49.840 -  Imperative_HOL/Imperative_HOL.thy \
  49.841 -  Imperative_HOL/Imperative_HOL_ex.thy \
  49.842 -  Imperative_HOL/Mrec.thy \
  49.843 -  Imperative_HOL/Ref.thy \
  49.844 -  Imperative_HOL/ROOT.ML \
  49.845 -  Imperative_HOL/ex/Imperative_Quicksort.thy \
  49.846 -  Imperative_HOL/ex/Imperative_Reverse.thy \
  49.847 -  Imperative_HOL/ex/Linked_Lists.thy \
  49.848 -  Imperative_HOL/ex/SatChecker.thy \
  49.849 -  Imperative_HOL/ex/Sorted_List.thy \
  49.850 -  Imperative_HOL/ex/Subarray.thy \
  49.851 -  Imperative_HOL/ex/Sublist.thy
  49.852 -	@$(ISABELLE_TOOL) usedir -g true -m iff -m no_brackets $(OUT)/HOL Imperative_HOL
  49.853 -
  49.854 -
  49.855 -## HOL-Decision_Procs
  49.856 -
  49.857 -HOL-Decision_Procs: HOL $(LOG)/HOL-Decision_Procs.gz
  49.858 -
  49.859 -$(LOG)/HOL-Decision_Procs.gz: $(OUT)/HOL \
  49.860 -  Library/Code_Integer.thy \
  49.861 -  Library/Code_Nat.thy \
  49.862 -  Library/Code_Natural.thy \
  49.863 -  Library/Efficient_Nat.thy \
  49.864 -  Decision_Procs/Approximation.thy \
  49.865 -  Decision_Procs/Commutative_Ring.thy \
  49.866 -  Decision_Procs/Commutative_Ring_Complete.thy \
  49.867 -  Decision_Procs/Cooper.thy \
  49.868 -  Decision_Procs/Decision_Procs.thy \
  49.869 -  Decision_Procs/Dense_Linear_Order.thy \
  49.870 -  Decision_Procs/Ferrack.thy \
  49.871 -  Decision_Procs/MIR.thy \
  49.872 -  Decision_Procs/Parametric_Ferrante_Rackoff.thy \
  49.873 -  Decision_Procs/Polynomial_List.thy \
  49.874 -  Decision_Procs/ROOT.ML \
  49.875 -  Decision_Procs/Reflected_Multivariate_Polynomial.thy \
  49.876 -  Decision_Procs/commutative_ring_tac.ML \
  49.877 -  Decision_Procs/cooper_tac.ML \
  49.878 -  Decision_Procs/ex/Approximation_Ex.thy \
  49.879 -  Decision_Procs/ex/Commutative_Ring_Ex.thy \
  49.880 -  Decision_Procs/ex/Dense_Linear_Order_Ex.thy \
  49.881 -  Decision_Procs/ferrack_tac.ML \
  49.882 -  Decision_Procs/ferrante_rackoff.ML \
  49.883 -  Decision_Procs/ferrante_rackoff_data.ML \
  49.884 -  Decision_Procs/langford.ML \
  49.885 -  Decision_Procs/langford_data.ML \
  49.886 -  Decision_Procs/mir_tac.ML
  49.887 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Decision_Procs
  49.888 -
  49.889 -
  49.890 -## HOL-Proofs
  49.891 -
  49.892 -HOL-Proofs: Pure $(OUT)/HOL-Proofs
  49.893 -
  49.894 -$(OUT)/HOL-Proofs: main.ML $(MAIN_DEPENDENCIES)
  49.895 -	@$(ISABELLE_TOOL) usedir -b -f main.ML -g true -p 2 -q 0 $(OUT)/Pure HOL-Proofs
  49.896 -
  49.897 -
  49.898 -## HOL-Proofs-ex
  49.899 -
  49.900 -HOL-Proofs-ex: HOL-Proofs $(LOG)/HOL-Proofs-ex.gz
  49.901 -
  49.902 -$(LOG)/HOL-Proofs-ex.gz: $(OUT)/HOL-Proofs			\
  49.903 -  Proofs/ex/ROOT.ML Proofs/ex/Hilbert_Classical.thy
  49.904 -	@cd Proofs; $(ISABELLE_TOOL) usedir -p 2 -q 0 $(OUT)/HOL-Proofs ex
  49.905 -
  49.906 -
  49.907 -## HOL-Proofs-Extraction
  49.908 -
  49.909 -HOL-Proofs-Extraction: HOL-Proofs $(LOG)/HOL-Proofs-Extraction.gz
  49.910 -
  49.911 -$(LOG)/HOL-Proofs-Extraction.gz: $(OUT)/HOL-Proofs		\
  49.912 -  Library/Code_Integer.thy Library/Code_Nat.thy			\
  49.913 -  Library/Code_Natural.thy Library/Efficient_Nat.thy		\
  49.914 -  Proofs/Extraction/Euclid.thy					\
  49.915 -  Proofs/Extraction/Greatest_Common_Divisor.thy			\
  49.916 -  Proofs/Extraction/Higman.thy					\
  49.917 -  Proofs/Extraction/Higman_Extraction.thy			\
  49.918 -  Proofs/Extraction/Pigeonhole.thy				\
  49.919 -  Proofs/Extraction/QuotRem.thy Proofs/Extraction/ROOT.ML	\
  49.920 -  Proofs/Extraction/Util.thy Proofs/Extraction/Warshall.thy	\
  49.921 -  Proofs/Extraction/document/root.tex				\
  49.922 -  Proofs/Extraction/document/root.bib
  49.923 -	@cd Proofs; $(ISABELLE_TOOL) usedir -p 2 -q 0 $(OUT)/HOL-Proofs Extraction
  49.924 -
  49.925 -
  49.926 -## HOL-Proofs-Lambda
  49.927 -
  49.928 -HOL-Proofs-Lambda: HOL-Proofs $(LOG)/HOL-Proofs-Lambda.gz
  49.929 -
  49.930 -$(LOG)/HOL-Proofs-Lambda.gz: $(OUT)/HOL-Proofs				\
  49.931 -  Proofs/Lambda/Commutation.thy Proofs/Lambda/Eta.thy			\
  49.932 -  Proofs/Lambda/InductTermi.thy Proofs/Lambda/Lambda.thy		\
  49.933 -  Proofs/Lambda/ListApplication.thy Proofs/Lambda/ListBeta.thy		\
  49.934 -  Proofs/Lambda/ListOrder.thy Proofs/Lambda/NormalForm.thy		\
  49.935 -  Proofs/Lambda/ParRed.thy Proofs/Lambda/Standardization.thy		\
  49.936 -  Proofs/Lambda/StrongNorm.thy Proofs/Lambda/Type.thy			\
  49.937 -  Proofs/Lambda/WeakNorm.thy Proofs/Lambda/ROOT.ML			\
  49.938 -  Proofs/Lambda/document/root.bib Proofs/Lambda/document/root.tex
  49.939 -	@cd Proofs; $(ISABELLE_TOOL) usedir -g true -m no_brackets -p 2 -q 0 $(OUT)/HOL-Proofs Lambda
  49.940 -
  49.941 -
  49.942 -## HOL-Prolog
  49.943 -
  49.944 -HOL-Prolog: HOL $(LOG)/HOL-Prolog.gz
  49.945 -
  49.946 -$(LOG)/HOL-Prolog.gz: $(OUT)/HOL Prolog/ROOT.ML Prolog/prolog.ML	\
  49.947 -  Prolog/HOHH.thy Prolog/Test.thy Prolog/Func.thy Prolog/Type.thy
  49.948 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Prolog
  49.949 -
  49.950 -
  49.951 -## HOL-MicroJava
  49.952 -
  49.953 -HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz
  49.954 -
  49.955 -$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL MicroJava/ROOT.ML			\
  49.956 -  MicroJava/Comp/AuxLemmas.thy MicroJava/Comp/CorrComp.thy		\
  49.957 -  MicroJava/Comp/CorrCompTp.thy MicroJava/Comp/DefsComp.thy		\
  49.958 -  MicroJava/Comp/Index.thy MicroJava/Comp/LemmasComp.thy		\
  49.959 -  MicroJava/Comp/TranslComp.thy MicroJava/Comp/TranslCompTp.thy		\
  49.960 -  MicroJava/Comp/TypeInf.thy MicroJava/J/Conform.thy			\
  49.961 -  MicroJava/J/Eval.thy MicroJava/J/JBasis.thy				\
  49.962 -  MicroJava/J/JTypeSafe.thy MicroJava/J/Decl.thy MicroJava/J/State.thy	\
  49.963 -  MicroJava/J/Term.thy MicroJava/J/Type.thy MicroJava/J/TypeRel.thy	\
  49.964 -  MicroJava/J/WellForm.thy MicroJava/J/Value.thy			\
  49.965 -  MicroJava/J/WellType.thy MicroJava/J/Example.thy			\
  49.966 -  MicroJava/J/JListExample.thy MicroJava/JVM/JVMExec.thy		\
  49.967 -  MicroJava/JVM/JVMInstructions.thy MicroJava/JVM/JVMState.thy		\
  49.968 -  MicroJava/JVM/JVMExecInstr.thy MicroJava/JVM/JVMListExample.thy	\
  49.969 -  MicroJava/JVM/JVMExceptions.thy MicroJava/DFA/Abstract_BV.thy		\
  49.970 -  MicroJava/DFA/Err.thy MicroJava/DFA/Kildall.thy			\
  49.971 -  MicroJava/DFA/LBVComplete.thy MicroJava/DFA/LBVCorrect.thy		\
  49.972 -  MicroJava/DFA/LBVSpec.thy MicroJava/DFA/Listn.thy			\
  49.973 -  MicroJava/DFA/Opt.thy MicroJava/DFA/Product.thy			\
  49.974 -  MicroJava/DFA/SemilatAlg.thy MicroJava/DFA/Semilat.thy		\
  49.975 -  MicroJava/DFA/Semilattices.thy					\
  49.976 -  MicroJava/DFA/Typing_Framework_err.thy				\
  49.977 -  MicroJava/DFA/Typing_Framework.thy MicroJava/BV/BVSpec.thy		\
  49.978 -  MicroJava/BV/BVSpecTypeSafe.thy MicroJava/BV/Correct.thy		\
  49.979 -  MicroJava/BV/JType.thy MicroJava/BV/JVM.thy MicroJava/BV/JVMType.thy	\
  49.980 -  MicroJava/BV/Effect.thy MicroJava/BV/EffectMono.thy			\
  49.981 -  MicroJava/BV/Typing_Framework_JVM.thy MicroJava/BV/BVExample.thy	\
  49.982 -  MicroJava/BV/LBVJVM.thy MicroJava/document/root.bib			\
  49.983 -  MicroJava/document/root.tex MicroJava/document/introduction.tex
  49.984 -	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL MicroJava
  49.985 -
  49.986 -
  49.987 -## HOL-NanoJava
  49.988 -
  49.989 -HOL-NanoJava: HOL $(LOG)/HOL-NanoJava.gz
  49.990 -
  49.991 -$(LOG)/HOL-NanoJava.gz: $(OUT)/HOL NanoJava/ROOT.ML NanoJava/Term.thy	\
  49.992 -  NanoJava/Decl.thy NanoJava/TypeRel.thy NanoJava/State.thy		\
  49.993 -  NanoJava/OpSem.thy NanoJava/AxSem.thy NanoJava/AxSem.thy		\
  49.994 -  NanoJava/document/root.bib NanoJava/document/root.tex
  49.995 -	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NanoJava
  49.996 -
  49.997 -
  49.998 -## HOL-Bali
  49.999 -
 49.1000 -HOL-Bali: HOL $(LOG)/HOL-Bali.gz
 49.1001 -
 49.1002 -$(LOG)/HOL-Bali.gz: $(OUT)/HOL Bali/AxCompl.thy Bali/AxExample.thy	\
 49.1003 -  Bali/AxSem.thy Bali/AxSound.thy Bali/Basis.thy Bali/Conform.thy	\
 49.1004 -  Bali/Decl.thy Bali/DeclConcepts.thy Bali/Eval.thy Bali/Evaln.thy	\
 49.1005 -  Bali/Example.thy Bali/Name.thy Bali/ROOT.ML Bali/State.thy		\
 49.1006 -  Bali/Table.thy Bali/Term.thy Bali/Trans.thy Bali/Type.thy		\
 49.1007 -  Bali/TypeRel.thy Bali/TypeSafe.thy Bali/Value.thy Bali/WellForm.thy	\
 49.1008 -  Bali/DefiniteAssignment.thy Bali/DefiniteAssignmentCorrect.thy	\
 49.1009 -  Bali/WellType.thy Bali/document/root.tex
 49.1010 -	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Bali
 49.1011 -
 49.1012 -
 49.1013 -## HOL-IOA
 49.1014 -
 49.1015 -HOL-IOA: HOL $(LOG)/HOL-IOA.gz
 49.1016 +HOL-IMP:
 49.1017 +	@$(ISABELLE_TOOL) build -b HOL-IMP
 49.1018  
 49.1019 -$(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.thy IOA/IOA.thy IOA/ROOT.ML	\
 49.1020 -  IOA/Solve.thy
 49.1021 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL IOA
 49.1022 -
 49.1023 -
 49.1024 -## HOL-Lattice
 49.1025 -
 49.1026 -HOL-Lattice: HOL $(LOG)/HOL-Lattice.gz
 49.1027 -
 49.1028 -$(LOG)/HOL-Lattice.gz: $(OUT)/HOL Lattice/Bounds.thy			\
 49.1029 -  Lattice/CompleteLattice.thy Lattice/Lattice.thy Lattice/Orders.thy	\
 49.1030 -  Lattice/ROOT.ML Lattice/document/root.tex
 49.1031 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Lattice
 49.1032 -
 49.1033 -
 49.1034 -## HOL-ex
 49.1035 -
 49.1036 -HOL-ex: HOL $(LOG)/HOL-ex.gz
 49.1037 -
 49.1038 -$(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy	\
 49.1039 -  Library/Code_Integer.thy Library/Code_Nat.thy				\
 49.1040 -  Library/Code_Natural.thy Library/Efficient_Nat.thy			\
 49.1041 -  Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy		\
 49.1042 -  ex/Arith_Examples.thy ex/BT.thy					\
 49.1043 -  ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradox.thy ex/CTL.thy		\
 49.1044 -  ex/Case_Product.thy ex/Chinese.thy ex/Classical.thy			\
 49.1045 -  ex/Code_Nat_examples.thy						\
 49.1046 -  ex/Coercion_Examples.thy ex/Coherent.thy ex/Dedekind_Real.thy		\
 49.1047 -  ex/Eval_Examples.thy ex/Executable_Relation.thy 			\
 49.1048 -  ex/FinFunPred.thy ex/Fundefs.thy					\
 49.1049 -  ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy	\
 49.1050 -  ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy		\
 49.1051 -  ex/Higher_Order_Logic.thy ex/Iff_Oracle.thy ex/Induction_Schema.thy	\
 49.1052 -  ex/Interpretation_with_Defs.thy ex/Intuitionistic.thy			\
 49.1053 -  ex/Lagrange.thy ex/List_to_Set_Comprehension_Examples.thy		\
 49.1054 -  ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy ex/Meson_Test.thy	\
 49.1055 -  ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy			\
 49.1056 -  ex/Normalization_by_Evaluation.thy ex/Numeral_Representation.thy	\
 49.1057 -  ex/Parallel_Example.thy						\
 49.1058 -  ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy				\
 49.1059 -  ex/Quicksort.thy ex/ROOT.ML						\
 49.1060 -  ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy		\
 49.1061 -  ex/SAT_Examples.thy ex/Serbian.thy 					\
 49.1062 -  ex/Set_Comprehension_Pointfree_Tests.thy ex/Set_Theory.thy		\
 49.1063 -  ex/Simproc_Tests.thy ex/SVC_Oracle.thy				\
 49.1064 -  ex/Seq.thy ex/Sqrt.thy ex/Sqrt_Script.thy 				\
 49.1065 -  ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy	\
 49.1066 -  ex/Transfer_Int_Nat.thy						\
 49.1067 -  ex/Tree23.thy	ex/Unification.thy ex/While_Combinator_Example.thy	\
 49.1068 -  ex/document/root.bib ex/document/root.tex ex/svc_funcs.ML		\
 49.1069 -  ex/svc_test.thy ../Tools/interpretation_with_defs.ML
 49.1070 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
 49.1071 -
 49.1072 -
 49.1073 -## HOL-Isar_Examples
 49.1074 -
 49.1075 -HOL-Isar_Examples: HOL $(LOG)/HOL-Isar_Examples.gz
 49.1076 -
 49.1077 -$(LOG)/HOL-Isar_Examples.gz: $(OUT)/HOL Isar_Examples/Basic_Logic.thy	\
 49.1078 -  Isar_Examples/Cantor.thy Isar_Examples/Drinker.thy			\
 49.1079 -  Isar_Examples/Expr_Compiler.thy Isar_Examples/Fibonacci.thy		\
 49.1080 -  Isar_Examples/Group.thy Isar_Examples/Group_Context.thy		\
 49.1081 -  Isar_Examples/Group_Notepad.thy Isar_Examples/Hoare.thy		\
 49.1082 -  Isar_Examples/Hoare_Ex.thy Isar_Examples/Knaster_Tarski.thy		\
 49.1083 -  Isar_Examples/Mutilated_Checkerboard.thy				\
 49.1084 -  Isar_Examples/Nested_Datatype.thy Isar_Examples/Peirce.thy		\
 49.1085 -  Isar_Examples/Puzzle.thy Isar_Examples/Summation.thy			\
 49.1086 -  Isar_Examples/ROOT.ML Isar_Examples/document/proof.sty		\
 49.1087 -  Isar_Examples/document/root.bib Isar_Examples/document/root.tex	\
 49.1088 -  Isar_Examples/document/style.tex Hoare/hoare_tac.ML			\
 49.1089 -  Number_Theory/Primes.thy
 49.1090 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Isar_Examples
 49.1091 -
 49.1092 -
 49.1093 -## HOL-SET_Protocol
 49.1094 -
 49.1095 -HOL-SET_Protocol: HOL $(LOG)/HOL-SET_Protocol.gz
 49.1096 -
 49.1097 -$(LOG)/HOL-SET_Protocol.gz: $(OUT)/HOL SET_Protocol/ROOT.ML		\
 49.1098 -  SET_Protocol/Message_SET.thy SET_Protocol/Event_SET.thy		\
 49.1099 -  SET_Protocol/Public_SET.thy SET_Protocol/Cardholder_Registration.thy	\
 49.1100 -  SET_Protocol/Merchant_Registration.thy SET_Protocol/Purchase.thy	\
 49.1101 -  SET_Protocol/SET_Protocol.thy SET_Protocol/document/root.tex
 49.1102 -	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL SET_Protocol
 49.1103 -
 49.1104 -
 49.1105 -## HOL-Matrix_LP
 49.1106 -
 49.1107 -HOL-Matrix_LP: HOL $(LOG)/HOL-Matrix_LP.gz
 49.1108 -
 49.1109 -$(LOG)/HOL-Matrix_LP.gz: $(OUT)/HOL Matrix_LP/ComputeFloat.thy		\
 49.1110 -  Matrix_LP/ComputeHOL.thy Matrix_LP/ComputeNumeral.thy			\
 49.1111 -  Matrix_LP/Compute_Oracle/Compute_Oracle.thy				\
 49.1112 -  Matrix_LP/Compute_Oracle/am.ML					\
 49.1113 -  Matrix_LP/Compute_Oracle/am_compiler.ML				\
 49.1114 -  Matrix_LP/Compute_Oracle/am_ghc.ML					\
 49.1115 -  Matrix_LP/Compute_Oracle/am_interpreter.ML				\
 49.1116 -  Matrix_LP/Compute_Oracle/am_sml.ML					\
 49.1117 -  Matrix_LP/Compute_Oracle/compute.ML					\
 49.1118 -  Matrix_LP/Compute_Oracle/linker.ML Matrix_LP/Cplex.thy		\
 49.1119 -  Matrix_LP/CplexMatrixConverter.ML Matrix_LP/Cplex_tools.ML		\
 49.1120 -  Matrix_LP/FloatSparseMatrixBuilder.ML Matrix_LP/LP.thy		\
 49.1121 -  Matrix_LP/Matrix.thy Matrix_LP/ROOT.ML Matrix_LP/SparseMatrix.thy	\
 49.1122 -  Matrix_LP/document/root.tex Matrix_LP/fspmlp.ML			\
 49.1123 -  Matrix_LP/matrixlp.ML Tools/float_arith.ML
 49.1124 -	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Matrix_LP
 49.1125 -
 49.1126 -
 49.1127 -## TLA
 49.1128 -
 49.1129 -TLA: HOL $(OUT)/TLA
 49.1130 -
 49.1131 -$(OUT)/TLA: $(OUT)/HOL TLA/Action.thy TLA/Init.thy TLA/Intensional.thy	\
 49.1132 -  TLA/ROOT.ML TLA/Stfun.thy TLA/TLA.thy
 49.1133 -	@cd TLA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL TLA
 49.1134 -
 49.1135 -
 49.1136 -## TLA-Inc
 49.1137 -
 49.1138 -TLA-Inc: TLA $(LOG)/TLA-Inc.gz
 49.1139 -
 49.1140 -$(LOG)/TLA-Inc.gz: $(OUT)/TLA TLA/Inc/Inc.thy
 49.1141 -	@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Inc
 49.1142 -
 49.1143 -
 49.1144 -## TLA-Buffer
 49.1145 -
 49.1146 -TLA-Buffer: TLA $(LOG)/TLA-Buffer.gz
 49.1147 -
 49.1148 -$(LOG)/TLA-Buffer.gz: $(OUT)/TLA TLA/Buffer/Buffer.thy	\
 49.1149 -  TLA/Buffer/DBuffer.thy
 49.1150 -	@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Buffer
 49.1151 -
 49.1152 -
 49.1153 -## TLA-Memory
 49.1154 -
 49.1155 -TLA-Memory: TLA $(LOG)/TLA-Memory.gz
 49.1156 -
 49.1157 -$(LOG)/TLA-Memory.gz: $(OUT)/TLA TLA/Memory/MemClerk.thy		\
 49.1158 -  TLA/Memory/MemClerkParameters.thy TLA/Memory/Memory.thy		\
 49.1159 -  TLA/Memory/MemoryImplementation.thy TLA/Memory/MemoryParameters.thy	\
 49.1160 -  TLA/Memory/ProcedureInterface.thy TLA/Memory/RPC.thy			\
 49.1161 -  TLA/Memory/RPCMemoryParams.thy TLA/Memory/RPCParameters.thy
 49.1162 -	@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Memory
 49.1163 -
 49.1164 -
 49.1165 -## HOL-TPTP
 49.1166 -
 49.1167 -HOL-TPTP: HOL $(LOG)/HOL-TPTP.gz
 49.1168 -
 49.1169 -$(LOG)/HOL-TPTP.gz: $(OUT)/HOL \
 49.1170 -  TPTP/ATP_Problem_Import.thy \
 49.1171 -  TPTP/ATP_Theory_Export.thy \
 49.1172 -  TPTP/MaSh_Eval.thy \
 49.1173 -  TPTP/MaSh_Export.thy \
 49.1174 -  TPTP/ROOT.ML \
 49.1175 -  TPTP/THF_Arith.thy \
 49.1176 -  TPTP/TPTP_Parser.thy \
 49.1177 -  TPTP/TPTP_Parser/ml_yacc_lib.ML \
 49.1178 -  TPTP/TPTP_Parser/tptp_interpret.ML \
 49.1179 -  TPTP/TPTP_Parser/tptp_lexyacc.ML \
 49.1180 -  TPTP/TPTP_Parser/tptp_parser.ML \
 49.1181 -  TPTP/TPTP_Parser/tptp_problem_name.ML \
 49.1182 -  TPTP/TPTP_Parser/tptp_syntax.ML \
 49.1183 -  TPTP/TPTP_Parser_Test.thy \
 49.1184 -  TPTP/atp_problem_import.ML \
 49.1185 -  TPTP/atp_theory_export.ML \
 49.1186 -  TPTP/mash_eval.ML \
 49.1187 -  TPTP/mash_export.ML \
 49.1188 -  TPTP/sledgehammer_tactics.ML
 49.1189 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL TPTP
 49.1190 -
 49.1191 -
 49.1192 -## HOL-Multivariate_Analysis
 49.1193 -
 49.1194 -HOL-Multivariate_Analysis: HOL $(OUT)/HOL-Multivariate_Analysis
 49.1195 +HOL-Multivariate_Analysis:
 49.1196 +	@$(ISABELLE_TOOL) build -b HOL-Multivariate_Analysis
 49.1197  
 49.1198 -$(OUT)/HOL-Multivariate_Analysis: $(OUT)/HOL				\
 49.1199 -  Multivariate_Analysis/Brouwer_Fixpoint.thy				\
 49.1200 -  Multivariate_Analysis/Cartesian_Euclidean_Space.thy			\
 49.1201 -  Multivariate_Analysis/Convex_Euclidean_Space.thy			\
 49.1202 -  Multivariate_Analysis/Derivative.thy					\
 49.1203 -  Multivariate_Analysis/Determinants.thy				\
 49.1204 -  Multivariate_Analysis/Euclidean_Space.thy				\
 49.1205 -  Multivariate_Analysis/Extended_Real_Limits.thy			\
 49.1206 -  Multivariate_Analysis/Fashoda.thy					\
 49.1207 -  Multivariate_Analysis/Finite_Cartesian_Product.thy			\
 49.1208 -  Multivariate_Analysis/Integration.certs				\
 49.1209 -  Multivariate_Analysis/Integration.thy					\
 49.1210 -  Multivariate_Analysis/L2_Norm.thy					\
 49.1211 -  Multivariate_Analysis/Linear_Algebra.thy				\
 49.1212 -  Multivariate_Analysis/Multivariate_Analysis.thy			\
 49.1213 -  Multivariate_Analysis/Norm_Arith.thy					\
 49.1214 -  Multivariate_Analysis/Operator_Norm.thy				\
 49.1215 -  Multivariate_Analysis/Path_Connected.thy				\
 49.1216 -  Multivariate_Analysis/ROOT.ML						\
 49.1217 -  Multivariate_Analysis/Real_Integration.thy				\
 49.1218 -  Multivariate_Analysis/Topology_Euclidean_Space.thy			\
 49.1219 -  Multivariate_Analysis/document/root.tex				\
 49.1220 -  Multivariate_Analysis/normarith.ML Library/Glbs.thy			\
 49.1221 -  Library/Extended_Real.thy Library/Indicator_Function.thy		\
 49.1222 -  Library/Inner_Product.thy Library/Numeral_Type.thy Library/Convex.thy	\
 49.1223 -  Library/FrechetDeriv.thy Library/Product_Vector.thy			\
 49.1224 -  Library/Product_plus.thy Library/Sum_of_Squares.thy
 49.1225 -	@cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Multivariate_Analysis
 49.1226 -
 49.1227 -
 49.1228 -## HOL-Probability
 49.1229 -
 49.1230 -HOL-Probability: HOL-Multivariate_Analysis $(OUT)/HOL-Probability
 49.1231 -
 49.1232 -$(OUT)/HOL-Probability: $(OUT)/HOL-Multivariate_Analysis		\
 49.1233 -  Probability/Binary_Product_Measure.thy Probability/Borel_Space.thy	\
 49.1234 -  Probability/Caratheodory.thy Probability/Complete_Measure.thy		\
 49.1235 -  Probability/ex/Dining_Cryptographers.thy				\
 49.1236 -  Probability/ex/Koepf_Duermuth_Countermeasure.thy			\
 49.1237 -  Probability/Finite_Product_Measure.thy				\
 49.1238 -  Probability/Independent_Family.thy					\
 49.1239 -  Probability/Infinite_Product_Measure.thy Probability/Information.thy	\
 49.1240 -  Probability/Lebesgue_Integration.thy Probability/Lebesgue_Measure.thy \
 49.1241 -  Probability/Measure_Space.thy Probability/Probability_Measure.thy	\
 49.1242 -  Probability/Probability.thy Probability/Radon_Nikodym.thy		\
 49.1243 -  Probability/ROOT.ML Probability/Sigma_Algebra.thy			\
 49.1244 -  Library/Countable.thy Library/FuncSet.thy Library/Nat_Bijection.thy
 49.1245 -	@cd Probability; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Multivariate_Analysis HOL-Probability
 49.1246 -
 49.1247 -
 49.1248 -## HOL-Nominal
 49.1249 -
 49.1250 -HOL-Nominal: HOL $(OUT)/HOL-Nominal
 49.1251 -
 49.1252 -$(OUT)/HOL-Nominal: $(OUT)/HOL Nominal/ROOT.ML \
 49.1253 -  Nominal/Nominal.thy \
 49.1254 -  Nominal/nominal_atoms.ML \
 49.1255 -  Nominal/nominal_datatype.ML \
 49.1256 -  Nominal/nominal_fresh_fun.ML \
 49.1257 -  Nominal/nominal_induct.ML \
 49.1258 -  Nominal/nominal_inductive.ML \
 49.1259 -  Nominal/nominal_inductive2.ML \
 49.1260 -  Nominal/nominal_permeq.ML \
 49.1261 -  Nominal/nominal_primrec.ML \
 49.1262 -  Nominal/nominal_thmdecls.ML \
 49.1263 -  Library/Infinite_Set.thy
 49.1264 -	@cd Nominal; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Nominal
 49.1265 -
 49.1266 -
 49.1267 -## HOL-Nominal-Examples
 49.1268 -
 49.1269 -HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz
 49.1270 -
 49.1271 -$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal \
 49.1272 -  Nominal/Examples/Nominal_Examples.thy \
 49.1273 -  Nominal/Examples/CK_Machine.thy \
 49.1274 -  Nominal/Examples/CR.thy \
 49.1275 -  Nominal/Examples/CR_Takahashi.thy \
 49.1276 -  Nominal/Examples/Class1.thy \
 49.1277 -  Nominal/Examples/Class2.thy \
 49.1278 -  Nominal/Examples/Class3.thy \
 49.1279 -  Nominal/Examples/Compile.thy \
 49.1280 -  Nominal/Examples/Contexts.thy \
 49.1281 -  Nominal/Examples/Crary.thy \
 49.1282 -  Nominal/Examples/Fsub.thy \
 49.1283 -  Nominal/Examples/Height.thy \
 49.1284 -  Nominal/Examples/Lam_Funs.thy \
 49.1285 -  Nominal/Examples/Lambda_mu.thy \
 49.1286 -  Nominal/Examples/LocalWeakening.thy \
 49.1287 -  Nominal/Examples/Pattern.thy \
 49.1288 -  Nominal/Examples/ROOT.ML \
 49.1289 -  Nominal/Examples/SN.thy \
 49.1290 -  Nominal/Examples/SOS.thy \
 49.1291 -  Nominal/Examples/Standardization.thy \
 49.1292 -  Nominal/Examples/Support.thy \
 49.1293 -  Nominal/Examples/Type_Preservation.thy \
 49.1294 -  Nominal/Examples/VC_Condition.thy \
 49.1295 -  Nominal/Examples/W.thy \
 49.1296 -  Nominal/Examples/Weakening.thy
 49.1297 -	@cd Nominal; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Nominal Examples
 49.1298 -
 49.1299 -
 49.1300 -## HOL-Word
 49.1301 -
 49.1302 -HOL-Word: HOL $(OUT)/HOL-Word
 49.1303 -
 49.1304 -$(OUT)/HOL-Word: $(OUT)/HOL Word/ROOT.ML Library/Boolean_Algebra.thy	\
 49.1305 -  Library/Numeral_Type.thy Word/Misc_Numeric.thy Word/Misc_Typedef.thy	\
 49.1306 -  Word/Type_Length.thy Word/Bit_Representation.thy Word/Bit_Int.thy	\
 49.1307 -  Word/Bool_List_Representation.thy Word/Bit_Operations.thy		\
 49.1308 -  Word/Word.thy Word/WordBitwise.thy Word/document/root.tex		\
 49.1309 -  Word/document/root.bib Word/Tools/smt_word.ML Word/Tools/word_lib.ML
 49.1310 -	@cd Word; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Word
 49.1311 -
 49.1312 -
 49.1313 -## HOL-Word-Examples
 49.1314 -
 49.1315 -HOL-Word-Examples: HOL-Word $(LOG)/HOL-Word-Examples.gz
 49.1316 -
 49.1317 -$(LOG)/HOL-Word-Examples.gz: $(OUT)/HOL-Word Word/Examples/ROOT.ML	\
 49.1318 -  Word/Examples/WordExamples.thy
 49.1319 -	@cd Word; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Word Examples
 49.1320 -
 49.1321 -
 49.1322 -## HOL-Statespace
 49.1323 -
 49.1324 -HOL-Statespace: HOL $(LOG)/HOL-Statespace.gz
 49.1325 -
 49.1326 -$(LOG)/HOL-Statespace.gz: $(OUT)/HOL Statespace/ROOT.ML			\
 49.1327 -  Statespace/DistinctTreeProver.thy Statespace/StateFun.thy		\
 49.1328 -  Statespace/StateSpaceLocale.thy Statespace/StateSpaceSyntax.thy	\
 49.1329 -  Statespace/StateSpaceEx.thy Statespace/distinct_tree_prover.ML	\
 49.1330 -  Statespace/state_space.ML Statespace/state_fun.ML			\
 49.1331 -  Statespace/document/root.tex
 49.1332 -	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Statespace
 49.1333 -
 49.1334 -
 49.1335 -## HOL-NSA
 49.1336 -
 49.1337 -HOL-NSA: HOL $(OUT)/HOL-NSA
 49.1338 -
 49.1339 -$(OUT)/HOL-NSA: $(OUT)/HOL NSA/CLim.thy NSA/CStar.thy NSA/NSCA.thy	\
 49.1340 -  NSA/NSComplex.thy NSA/HDeriv.thy NSA/HLim.thy NSA/HLog.thy		\
 49.1341 -  NSA/HSEQ.thy NSA/HSeries.thy NSA/HTranscendental.thy			\
 49.1342 -  NSA/Hypercomplex.thy NSA/HyperDef.thy NSA/HyperNat.thy		\
 49.1343 -  NSA/Hyperreal.thy NSA/Filter.thy NSA/NatStar.thy NSA/NSA.thy		\
 49.1344 -  NSA/StarDef.thy NSA/Star.thy NSA/transfer.ML				\
 49.1345 -  Library/Infinite_Set.thy Library/Zorn.thy NSA/ROOT.ML
 49.1346 -	@cd NSA; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-NSA
 49.1347 -
 49.1348 -
 49.1349 -## HOL-NSA-Examples
 49.1350 -
 49.1351 -HOL-NSA-Examples: HOL-NSA $(LOG)/HOL-NSA-Examples.gz
 49.1352 -
 49.1353 -$(LOG)/HOL-NSA-Examples.gz: $(OUT)/HOL-NSA NSA/Examples/ROOT.ML		\
 49.1354 -  NSA/Examples/NSPrimes.thy
 49.1355 -	@cd NSA; $(ISABELLE_TOOL) usedir $(OUT)/HOL-NSA Examples
 49.1356 -
 49.1357 -
 49.1358 -## HOL-Mirabelle
 49.1359 -
 49.1360 -HOL-Mirabelle: HOL $(LOG)/HOL-Mirabelle.gz
 49.1361 -
 49.1362 -$(LOG)/HOL-Mirabelle.gz: $(OUT)/HOL Mirabelle/Mirabelle_Test.thy \
 49.1363 -  Mirabelle/Mirabelle.thy Mirabelle/Tools/mirabelle.ML \
 49.1364 -  Mirabelle/ROOT.ML Mirabelle/Tools/mirabelle_arith.ML \
 49.1365 -  Mirabelle/Tools/mirabelle_metis.ML \
 49.1366 -  Mirabelle/Tools/mirabelle_quickcheck.ML \
 49.1367 -  Mirabelle/Tools/mirabelle_refute.ML	\
 49.1368 -  Mirabelle/Tools/mirabelle_sledgehammer.ML \
 49.1369 -  Mirabelle/Tools/mirabelle_sledgehammer_filter.ML \
 49.1370 -  Mirabelle/Tools/mirabelle_try0.ML \
 49.1371 -  TPTP/sledgehammer_tactics.ML Mirabelle/lib/Tools/mirabelle \
 49.1372 -  Mirabelle/lib/scripts/mirabelle.pl Library/FrechetDeriv.thy \
 49.1373 -  Library/Inner_Product.thy
 49.1374 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle
 49.1375 -	@cd Library; $(ISABELLE_TOOL) mirabelle -q arith Inner_Product.thy # some arbitrary small test case
 49.1376 -
 49.1377 -
 49.1378 -## HOL-Word-SMT_Examples
 49.1379 -
 49.1380 -HOL-Word-SMT_Examples: HOL-Word $(LOG)/HOL-Word-SMT_Examples.gz
 49.1381 -
 49.1382 -$(LOG)/HOL-Word-SMT_Examples.gz: $(OUT)/HOL-Word SMT_Examples/ROOT.ML	\
 49.1383 -  SMT_Examples/SMT_Examples.thy SMT_Examples/SMT_Examples.certs		\
 49.1384 -  SMT_Examples/SMT_Word_Examples.thy SMT_Examples/SMT_Tests.thy		\
 49.1385 -  SMT_Examples/SMT_Word_Examples.certs SMT_Examples/SMT_Tests.certs
 49.1386 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL-Word SMT_Examples
 49.1387 -
 49.1388 -
 49.1389 -## HOL-Boogie
 49.1390 -
 49.1391 -HOL-Boogie: HOL-Word $(OUT)/HOL-Boogie
 49.1392 -
 49.1393 -$(OUT)/HOL-Boogie: $(OUT)/HOL-Word Boogie/ROOT.ML Boogie/Boogie.thy	\
 49.1394 -  Boogie/Tools/boogie_vcs.ML Boogie/Tools/boogie_loader.ML		\
 49.1395 -  Boogie/Tools/boogie_commands.ML Boogie/Tools/boogie_tactics.ML
 49.1396 -	@cd Boogie; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-Boogie
 49.1397 -
 49.1398 -
 49.1399 -## HOL-Boogie_Examples
 49.1400 -
 49.1401 -HOL-Boogie-Examples: HOL-Boogie $(LOG)/HOL-Boogie-Examples.gz
 49.1402 -
 49.1403 -$(LOG)/HOL-Boogie-Examples.gz: $(OUT)/HOL-Boogie			\
 49.1404 -  Boogie/Examples/ROOT.ML Boogie/Examples/Boogie_Max.thy		\
 49.1405 -  Boogie/Examples/Boogie_Max.b2i Boogie/Examples/Boogie_Dijkstra.thy	\
 49.1406 -  Boogie/Examples/VCC_Max.thy Boogie/Examples/Boogie_Dijkstra.b2i	\
 49.1407 -  Boogie/Examples/VCC_Max.b2i Boogie/Examples/Boogie_Max.certs		\
 49.1408 -  Boogie/Examples/Boogie_Dijkstra.certs Boogie/Examples/VCC_Max.certs
 49.1409 -	@cd Boogie; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Boogie Examples
 49.1410 -
 49.1411 -
 49.1412 -## HOL-SPARK
 49.1413 -
 49.1414 -HOL-SPARK: HOL-Word $(OUT)/HOL-SPARK
 49.1415 -
 49.1416 -$(OUT)/HOL-SPARK: $(OUT)/HOL-Word SPARK/ROOT.ML 		\
 49.1417 -  SPARK/SPARK.thy SPARK/SPARK_Setup.thy				\
 49.1418 -  SPARK/Tools/fdl_lexer.ML SPARK/Tools/fdl_parser.ML		\
 49.1419 -  SPARK/Tools/spark_commands.ML SPARK/Tools/spark_vcs.ML
 49.1420 -	@cd SPARK; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SPARK
 49.1421 -
 49.1422 -
 49.1423 -## HOL-SPARK-Examples
 49.1424 -
 49.1425 -HOL-SPARK-Examples: HOL-SPARK $(LOG)/HOL-SPARK-Examples.gz
 49.1426 +HOL-Nominal:
 49.1427 +	@$(ISABELLE_TOOL) build -b HOL-Nominal
 49.1428  
 49.1429 -$(LOG)/HOL-SPARK-Examples.gz: $(OUT)/HOL-SPARK				\
 49.1430 -  SPARK/Examples/ROOT.ML						\
 49.1431 -  SPARK/Examples/Gcd/Greatest_Common_Divisor.thy			\
 49.1432 -  SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.fdl			\
 49.1433 -  SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.rls			\
 49.1434 -  SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.siv			\
 49.1435 -  SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy		\
 49.1436 -  SPARK/Examples/Liseq/liseq/liseq_length.fdl				\
 49.1437 -  SPARK/Examples/Liseq/liseq/liseq_length.rls				\
 49.1438 -  SPARK/Examples/Liseq/liseq/liseq_length.siv				\
 49.1439 -  SPARK/Examples/RIPEMD-160/F.thy SPARK/Examples/RIPEMD-160/Hash.thy	\
 49.1440 -  SPARK/Examples/RIPEMD-160/K_L.thy SPARK/Examples/RIPEMD-160/K_R.thy	\
 49.1441 -  SPARK/Examples/RIPEMD-160/R_L.thy					\
 49.1442 -  SPARK/Examples/RIPEMD-160/RMD_Lemmas.thy				\
 49.1443 -  SPARK/Examples/RIPEMD-160/RMD_Specification.thy			\
 49.1444 -  SPARK/Examples/RIPEMD-160/RMD.thy SPARK/Examples/RIPEMD-160/Round.thy	\
 49.1445 -  SPARK/Examples/RIPEMD-160/R_R.thy SPARK/Examples/RIPEMD-160/S_L.thy	\
 49.1446 -  SPARK/Examples/RIPEMD-160/S_R.thy					\
 49.1447 -  SPARK/Examples/RIPEMD-160/rmd/f.fdl					\
 49.1448 -  SPARK/Examples/RIPEMD-160/rmd/f.rls					\
 49.1449 -  SPARK/Examples/RIPEMD-160/rmd/f.siv					\
 49.1450 -  SPARK/Examples/RIPEMD-160/rmd/hash.fdl				\
 49.1451 -  SPARK/Examples/RIPEMD-160/rmd/hash.rls				\
 49.1452 -  SPARK/Examples/RIPEMD-160/rmd/hash.siv				\
 49.1453 -  SPARK/Examples/RIPEMD-160/rmd/k_l.fdl					\
 49.1454 -  SPARK/Examples/RIPEMD-160/rmd/k_l.rls					\
 49.1455 -  SPARK/Examples/RIPEMD-160/rmd/k_l.siv					\
 49.1456 -  SPARK/Examples/RIPEMD-160/rmd/k_r.fdl					\
 49.1457 -  SPARK/Examples/RIPEMD-160/rmd/k_r.rls					\
 49.1458 -  SPARK/Examples/RIPEMD-160/rmd/k_r.siv					\
 49.1459 -  SPARK/Examples/RIPEMD-160/rmd/r_l.fdl					\
 49.1460 -  SPARK/Examples/RIPEMD-160/rmd/r_l.rls					\
 49.1461 -  SPARK/Examples/RIPEMD-160/rmd/r_l.siv					\
 49.1462 -  SPARK/Examples/RIPEMD-160/rmd/round.fdl				\
 49.1463 -  SPARK/Examples/RIPEMD-160/rmd/round.rls				\
 49.1464 -  SPARK/Examples/RIPEMD-160/rmd/round.siv				\
 49.1465 -  SPARK/Examples/RIPEMD-160/rmd/r_r.fdl					\
 49.1466 -  SPARK/Examples/RIPEMD-160/rmd/r_r.rls					\
 49.1467 -  SPARK/Examples/RIPEMD-160/rmd/r_r.siv					\
 49.1468 -  SPARK/Examples/RIPEMD-160/rmd/s_l.fdl					\
 49.1469 -  SPARK/Examples/RIPEMD-160/rmd/s_l.rls					\
 49.1470 -  SPARK/Examples/RIPEMD-160/rmd/s_l.siv					\
 49.1471 -  SPARK/Examples/RIPEMD-160/rmd/s_r.fdl					\
 49.1472 -  SPARK/Examples/RIPEMD-160/rmd/s_r.rls					\
 49.1473 -  SPARK/Examples/RIPEMD-160/rmd/s_r.siv
 49.1474 -	@cd SPARK; $(ISABELLE_TOOL) usedir $(OUT)/HOL-SPARK Examples
 49.1475 -
 49.1476 -
 49.1477 -## HOL-SPARK-Manual
 49.1478 -
 49.1479 -HOL-SPARK-Manual: HOL-SPARK $(LOG)/HOL-SPARK-Manual.gz
 49.1480 -
 49.1481 -$(LOG)/HOL-SPARK-Manual.gz: $(OUT)/HOL-SPARK				\
 49.1482 -  SPARK/Manual/ROOT.ML							\
 49.1483 -  SPARK/Manual/Complex_Types.thy					\
 49.1484 -  SPARK/Manual/Example_Verification.thy					\
 49.1485 -  SPARK/Manual/Proc1.thy						\
 49.1486 -  SPARK/Manual/Proc2.thy						\
 49.1487 -  SPARK/Manual/Reference.thy						\
 49.1488 -  SPARK/Manual/Simple_Greatest_Common_Divisor.thy			\
 49.1489 -  SPARK/Manual/VC_Principles.thy					\
 49.1490 -  SPARK/Manual/complex_types_app/initialize.fdl				\
 49.1491 -  SPARK/Manual/complex_types_app/initialize.rls				\
 49.1492 -  SPARK/Manual/complex_types_app/initialize.siv				\
 49.1493 -  SPARK/Manual/loop_invariant/proc1.fdl					\
 49.1494 -  SPARK/Manual/loop_invariant/proc1.rls					\
 49.1495 -  SPARK/Manual/loop_invariant/proc1.siv					\
 49.1496 -  SPARK/Manual/loop_invariant/proc2.fdl					\
 49.1497 -  SPARK/Manual/loop_invariant/proc2.rls					\
 49.1498 -  SPARK/Manual/loop_invariant/proc2.siv					\
 49.1499 -  SPARK/Manual/simple_greatest_common_divisor/g_c_d.fdl			\
 49.1500 -  SPARK/Manual/simple_greatest_common_divisor/g_c_d.rls			\
 49.1501 -  SPARK/Manual/simple_greatest_common_divisor/g_c_d.siv			\
 49.1502 -  SPARK/Manual/document/complex_types.ads				\
 49.1503 -  SPARK/Manual/document/complex_types_app.adb				\
 49.1504 -  SPARK/Manual/document/complex_types_app.ads				\
 49.1505 -  SPARK/Manual/document/loop_invariant.adb				\
 49.1506 -  SPARK/Manual/document/loop_invariant.ads				\
 49.1507 -  SPARK/Manual/document/Simple_Gcd.adb					\
 49.1508 -  SPARK/Manual/document/Simple_Gcd.ads					\
 49.1509 -  SPARK/Manual/document/intro.tex					\
 49.1510 -  SPARK/Manual/document/root.tex					\
 49.1511 -  SPARK/Manual/document/root.bib					\
 49.1512 -  SPARK/Examples/Gcd/Greatest_Common_Divisor.thy			\
 49.1513 -  SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.fdl			\
 49.1514 -  SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.rls			\
 49.1515 -  SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.siv
 49.1516 -	@cd SPARK; $(ISABELLE_TOOL) usedir $(OUT)/HOL-SPARK Manual
 49.1517 -
 49.1518 -
 49.1519 -## HOL-Mutabelle
 49.1520 -
 49.1521 -HOL-Mutabelle: HOL $(LOG)/HOL-Mutabelle.gz
 49.1522 -
 49.1523 -$(LOG)/HOL-Mutabelle.gz: $(OUT)/HOL Mutabelle/MutabelleExtra.thy	\
 49.1524 -  Mutabelle/ROOT.ML Mutabelle/mutabelle.ML				\
 49.1525 -  Mutabelle/mutabelle_extra.ML
 49.1526 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mutabelle
 49.1527 -
 49.1528 -## HOL-Quickcheck_Examples
 49.1529 -
 49.1530 -HOL-Quickcheck_Examples: HOL $(LOG)/HOL-Quickcheck_Examples.gz
 49.1531 -
 49.1532 -$(LOG)/HOL-Quickcheck_Examples.gz: $(OUT)/HOL				\
 49.1533 -  Quickcheck_Examples/ROOT.ML						\
 49.1534 -  Quickcheck_Examples/Completeness.thy					\
 49.1535 -  Quickcheck_Examples/Hotel_Example.thy					\
 49.1536 -  Quickcheck_Examples/Quickcheck_Examples.thy				\
 49.1537 -  Quickcheck_Examples/Quickcheck_Interfaces.thy				\
 49.1538 -  Quickcheck_Examples/Quickcheck_Lattice_Examples.thy			\
 49.1539 -  Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy
 49.1540 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quickcheck_Examples
 49.1541 -
 49.1542 -## HOL-Quotient_Examples
 49.1543 -
 49.1544 -HOL-Quotient_Examples: HOL $(LOG)/HOL-Quotient_Examples.gz
 49.1545 -
 49.1546 -$(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL				\
 49.1547 -  Quotient_Examples/DList.thy \
 49.1548 -  Quotient_Examples/FSet.thy \
 49.1549 -  Quotient_Examples/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy \
 49.1550 -  Quotient_Examples/Lift_FSet.thy \
 49.1551 -  Quotient_Examples/Lift_Set.thy \
 49.1552 -  Quotient_Examples/Lift_Fun.thy Quotient_Examples/Lift_DList.thy
 49.1553 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples
 49.1554 -
 49.1555 -
 49.1556 -## HOL-Predicate_Compile_Examples
 49.1557 -
 49.1558 -HOL-Predicate_Compile_Examples: HOL $(LOG)/HOL-Predicate_Compile_Examples.gz
 49.1559 -
 49.1560 -$(LOG)/HOL-Predicate_Compile_Examples.gz: $(OUT)/HOL			\
 49.1561 -  Predicate_Compile_Examples/ROOT.ML					\
 49.1562 -  Predicate_Compile_Examples/Predicate_Compile_Tests.thy		\
 49.1563 -  Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy  \
 49.1564 -  Predicate_Compile_Examples/Code_Prolog_Examples.thy 			\
 49.1565 -  Predicate_Compile_Examples/Examples.thy				\
 49.1566 -  Predicate_Compile_Examples/Context_Free_Grammar_Example.thy 		\
 49.1567 -  Predicate_Compile_Examples/Hotel_Example.thy 				\
 49.1568 -  Predicate_Compile_Examples/Hotel_Example_Prolog.thy 			\
 49.1569 -  Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy 		\
 49.1570 -  Predicate_Compile_Examples/IMP_1.thy 					\
 49.1571 -  Predicate_Compile_Examples/IMP_2.thy 					\
 49.1572 -  Predicate_Compile_Examples/IMP_3.thy 					\
 49.1573 -  Predicate_Compile_Examples/IMP_4.thy 					\
 49.1574 -  Predicate_Compile_Examples/Lambda_Example.thy 			\
 49.1575 -  Predicate_Compile_Examples/List_Examples.thy 				\
 49.1576 -  Predicate_Compile_Examples/Reg_Exp_Example.thy
 49.1577 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Predicate_Compile_Examples
 49.1578 -
 49.1579 -
 49.1580 -## HOLCF
 49.1581 -
 49.1582 -HOLCF: HOL $(OUT)/HOLCF
 49.1583 -
 49.1584 -$(OUT)/HOLCF: $(OUT)/HOL \
 49.1585 -  HOLCF/ROOT.ML \
 49.1586 -  HOLCF/Adm.thy \
 49.1587 -  HOLCF/Algebraic.thy \
 49.1588 -  HOLCF/Bifinite.thy \
 49.1589 -  HOLCF/Cfun.thy \
 49.1590 -  HOLCF/Compact_Basis.thy \
 49.1591 -  HOLCF/Completion.thy \
 49.1592 -  HOLCF/Cont.thy \
 49.1593 -  HOLCF/ConvexPD.thy \
 49.1594 -  HOLCF/Cpodef.thy \
 49.1595 -  HOLCF/Cprod.thy \
 49.1596 -  HOLCF/Discrete.thy \
 49.1597 -  HOLCF/Deflation.thy \
 49.1598 -  HOLCF/Domain.thy \
 49.1599 -  HOLCF/Domain_Aux.thy \
 49.1600 -  HOLCF/Fixrec.thy \
 49.1601 -  HOLCF/Fix.thy \
 49.1602 -  HOLCF/Fun_Cpo.thy \
 49.1603 -  HOLCF/HOLCF.thy \
 49.1604 -  HOLCF/Lift.thy \
 49.1605 -  HOLCF/LowerPD.thy \
 49.1606 -  HOLCF/Map_Functions.thy \
 49.1607 -  HOLCF/One.thy \
 49.1608 -  HOLCF/Pcpo.thy \
 49.1609 -  HOLCF/Plain_HOLCF.thy \
 49.1610 -  HOLCF/Porder.thy \
 49.1611 -  HOLCF/Powerdomains.thy \
 49.1612 -  HOLCF/Product_Cpo.thy \
 49.1613 -  HOLCF/Representable.thy \
 49.1614 -  HOLCF/Sfun.thy \
 49.1615 -  HOLCF/Sprod.thy \
 49.1616 -  HOLCF/Ssum.thy \
 49.1617 -  HOLCF/Tr.thy \
 49.1618 -  HOLCF/Universal.thy \
 49.1619 -  HOLCF/UpperPD.thy \
 49.1620 -  HOLCF/Up.thy \
 49.1621 -  HOLCF/Tools/cont_consts.ML \
 49.1622 -  HOLCF/Tools/cont_proc.ML \
 49.1623 -  HOLCF/Tools/holcf_library.ML \
 49.1624 -  HOLCF/Tools/Domain/domain.ML \
 49.1625 -  HOLCF/Tools/Domain/domain_axioms.ML \
 49.1626 -  HOLCF/Tools/Domain/domain_constructors.ML \
 49.1627 -  HOLCF/Tools/Domain/domain_induction.ML \
 49.1628 -  HOLCF/Tools/Domain/domain_isomorphism.ML \
 49.1629 -  HOLCF/Tools/Domain/domain_take_proofs.ML \
 49.1630 -  HOLCF/Tools/cpodef.ML \
 49.1631 -  HOLCF/Tools/domaindef.ML \
 49.1632 -  HOLCF/Tools/fixrec.ML \
 49.1633 -  HOLCF/document/root.tex
 49.1634 -	@cd HOLCF; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOLCF
 49.1635 -
 49.1636 -
 49.1637 -## HOLCF-Tutorial
 49.1638 -
 49.1639 -HOLCF-Tutorial: HOLCF $(LOG)/HOLCF-Tutorial.gz
 49.1640 -
 49.1641 -$(LOG)/HOLCF-Tutorial.gz: $(OUT)/HOLCF \
 49.1642 -  HOLCF/Tutorial/Domain_ex.thy \
 49.1643 -  HOLCF/Tutorial/Fixrec_ex.thy \
 49.1644 -  HOLCF/Tutorial/New_Domain.thy \
 49.1645 -  HOLCF/Tutorial/document/root.tex \
 49.1646 -  HOLCF/Tutorial/ROOT.ML
 49.1647 -	@cd HOLCF; $(ISABELLE_TOOL) usedir $(OUT)/HOLCF Tutorial
 49.1648 -
 49.1649 -
 49.1650 -## HOLCF-Library
 49.1651 -
 49.1652 -HOLCF-Library: HOLCF $(LOG)/HOLCF-Library.gz
 49.1653 +HOL-Word:
 49.1654 +	@$(ISABELLE_TOOL) build -b HOL-Word
 49.1655  
 49.1656 -$(LOG)/HOLCF-Library.gz: $(OUT)/HOLCF \
 49.1657 -  Library/Extended_Nat.thy \
 49.1658 -  HOLCF/Library/Defl_Bifinite.thy \
 49.1659 -  HOLCF/Library/Bool_Discrete.thy \
 49.1660 -  HOLCF/Library/Char_Discrete.thy \
 49.1661 -  HOLCF/Library/HOL_Cpo.thy \
 49.1662 -  HOLCF/Library/Int_Discrete.thy \
 49.1663 -  HOLCF/Library/List_Cpo.thy \
 49.1664 -  HOLCF/Library/List_Predomain.thy \
 49.1665 -  HOLCF/Library/Nat_Discrete.thy \
 49.1666 -  HOLCF/Library/Option_Cpo.thy \
 49.1667 -  HOLCF/Library/Stream.thy \
 49.1668 -  HOLCF/Library/Sum_Cpo.thy \
 49.1669 -  HOLCF/Library/HOLCF_Library.thy \
 49.1670 -  HOLCF/Library/ROOT.ML
 49.1671 -	@cd HOLCF; $(ISABELLE_TOOL) usedir $(OUT)/HOLCF Library
 49.1672 -
 49.1673 -
 49.1674 -## HOLCF-IMP
 49.1675 -
 49.1676 -HOLCF-IMP: HOLCF $(LOG)/HOLCF-IMP.gz
 49.1677 -
 49.1678 -$(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF \
 49.1679 -  HOLCF/IMP/HoareEx.thy \
 49.1680 -  HOLCF/IMP/Denotational.thy \
 49.1681 -  HOLCF/IMP/ROOT.ML \
 49.1682 -  HOLCF/IMP/document/root.tex
 49.1683 -	@cd HOLCF; $(ISABELLE_TOOL) usedir $(OUT)/HOLCF IMP
 49.1684 -
 49.1685 -
 49.1686 -## HOLCF-ex
 49.1687 -
 49.1688 -HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz
 49.1689 -
 49.1690 -$(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF \
 49.1691 -  HOLCF/ex/Concurrency_Monad.thy \
 49.1692 -  HOLCF/ex/Dagstuhl.thy \
 49.1693 -  HOLCF/ex/Dnat.thy \
 49.1694 -  HOLCF/ex/Domain_Proofs.thy \
 49.1695 -  HOLCF/ex/Fix2.thy \
 49.1696 -  HOLCF/ex/Focus_ex.thy \
 49.1697 -  HOLCF/ex/Hoare.thy \
 49.1698 -  HOLCF/ex/Letrec.thy \
 49.1699 -  HOLCF/ex/Loop.thy \
 49.1700 -  HOLCF/ex/Pattern_Match.thy \
 49.1701 -  HOLCF/ex/Powerdomain_ex.thy \
 49.1702 -  HOLCF/ex/ROOT.ML
 49.1703 -	@cd HOLCF; $(ISABELLE_TOOL) usedir $(OUT)/HOLCF ex
 49.1704 -
 49.1705 -
 49.1706 -## HOLCF-FOCUS
 49.1707 -
 49.1708 -HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz
 49.1709 -
 49.1710 -$(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF HOLCF/FOCUS/ROOT.ML \
 49.1711 -  Library/Extended_Nat.thy \
 49.1712 -  HOLCF/Library/Stream.thy \
 49.1713 -  HOLCF/FOCUS/Fstreams.thy \
 49.1714 -  HOLCF/FOCUS/Fstream.thy \
 49.1715 -  HOLCF/FOCUS/FOCUS.thy \
 49.1716 -  HOLCF/FOCUS/Stream_adm.thy \
 49.1717 -  HOLCF/FOCUS/Buffer.thy \
 49.1718 -  HOLCF/FOCUS/Buffer_adm.thy \
 49.1719 -  Library/Continuity.thy
 49.1720 -	@cd HOLCF; $(ISABELLE_TOOL) usedir $(OUT)/HOLCF FOCUS
 49.1721 -
 49.1722 -
 49.1723 -## IOA
 49.1724 -
 49.1725 -IOA: HOLCF $(OUT)/IOA
 49.1726 -
 49.1727 -$(OUT)/IOA: $(OUT)/HOLCF \
 49.1728 -  HOLCF/IOA/ROOT.ML \
 49.1729 -  HOLCF/IOA/meta_theory/Traces.thy \
 49.1730 -  HOLCF/IOA/meta_theory/Asig.thy \
 49.1731 -  HOLCF/IOA/meta_theory/CompoScheds.thy \
 49.1732 -  HOLCF/IOA/meta_theory/CompoTraces.thy \
 49.1733 -  HOLCF/IOA/meta_theory/Seq.thy \
 49.1734 -  HOLCF/IOA/meta_theory/RefCorrectness.thy \
 49.1735 -  HOLCF/IOA/meta_theory/Automata.thy \
 49.1736 -  HOLCF/IOA/meta_theory/ShortExecutions.thy \
 49.1737 -  HOLCF/IOA/meta_theory/IOA.thy \
 49.1738 -  HOLCF/IOA/meta_theory/Sequence.thy \
 49.1739 -  HOLCF/IOA/meta_theory/CompoExecs.thy \
 49.1740 -  HOLCF/IOA/meta_theory/RefMappings.thy \
 49.1741 -  HOLCF/IOA/meta_theory/Compositionality.thy \
 49.1742 -  HOLCF/IOA/meta_theory/TL.thy \
 49.1743 -  HOLCF/IOA/meta_theory/TLS.thy \
 49.1744 -  HOLCF/IOA/meta_theory/LiveIOA.thy \
 49.1745 -  HOLCF/IOA/meta_theory/Pred.thy \
 49.1746 -  HOLCF/IOA/meta_theory/Abstraction.thy \
 49.1747 -  HOLCF/IOA/meta_theory/Simulations.thy \
 49.1748 -  HOLCF/IOA/meta_theory/SimCorrectness.thy
 49.1749 -	@cd HOLCF/IOA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOLCF IOA
 49.1750 -
 49.1751 -
 49.1752 -## IOA-ABP
 49.1753 -
 49.1754 -IOA-ABP: IOA $(LOG)/IOA-ABP.gz
 49.1755 -
 49.1756 -$(LOG)/IOA-ABP.gz: $(OUT)/IOA \
 49.1757 -  HOLCF/IOA/ABP/Abschannel.thy \
 49.1758 -  HOLCF/IOA/ABP/Abschannel_finite.thy \
 49.1759 -  HOLCF/IOA/ABP/Action.thy \
 49.1760 -  HOLCF/IOA/ABP/Check.ML \
 49.1761 -  HOLCF/IOA/ABP/Correctness.thy \
 49.1762 -  HOLCF/IOA/ABP/Env.thy \
 49.1763 -  HOLCF/IOA/ABP/Impl.thy \
 49.1764 -  HOLCF/IOA/ABP/Impl_finite.thy \
 49.1765 -  HOLCF/IOA/ABP/Lemmas.thy \
 49.1766 -  HOLCF/IOA/ABP/Packet.thy \
 49.1767 -  HOLCF/IOA/ABP/ROOT.ML \
 49.1768 -  HOLCF/IOA/ABP/Receiver.thy \
 49.1769 -  HOLCF/IOA/ABP/Sender.thy \
 49.1770 -  HOLCF/IOA/ABP/Spec.thy
 49.1771 -	@cd HOLCF/IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ABP
 49.1772 -
 49.1773 -
 49.1774 -## IOA-NTP
 49.1775 -
 49.1776 -IOA-NTP: IOA $(LOG)/IOA-NTP.gz
 49.1777 +HOLCF:
 49.1778 +	@$(ISABELLE_TOOL) build -b HOLCF
 49.1779  
 49.1780 -$(LOG)/IOA-NTP.gz: $(OUT)/IOA \
 49.1781 -  HOLCF/IOA/NTP/Abschannel.thy \
 49.1782 -  HOLCF/IOA/NTP/Action.thy \
 49.1783 -  HOLCF/IOA/NTP/Correctness.thy \
 49.1784 -  HOLCF/IOA/NTP/Impl.thy \
 49.1785 -  HOLCF/IOA/NTP/Lemmas.thy \
 49.1786 -  HOLCF/IOA/NTP/Multiset.thy \
 49.1787 -  HOLCF/IOA/NTP/Packet.thy \
 49.1788 -  HOLCF/IOA/NTP/ROOT.ML \
 49.1789 -  HOLCF/IOA/NTP/Receiver.thy \
 49.1790 -  HOLCF/IOA/NTP/Sender.thy \
 49.1791 -  HOLCF/IOA/NTP/Spec.thy
 49.1792 -	@cd HOLCF/IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA NTP
 49.1793 -
 49.1794 -
 49.1795 -## IOA-Storage
 49.1796 -
 49.1797 -IOA-Storage: IOA $(LOG)/IOA-Storage.gz
 49.1798 -
 49.1799 -$(LOG)/IOA-Storage.gz: $(OUT)/IOA \
 49.1800 -  HOLCF/IOA/Storage/Action.thy \
 49.1801 -  HOLCF/IOA/Storage/Correctness.thy \
 49.1802 -  HOLCF/IOA/Storage/Impl.thy \
 49.1803 -  HOLCF/IOA/Storage/ROOT.ML \
 49.1804 -  HOLCF/IOA/Storage/Spec.thy
 49.1805 -	@cd HOLCF/IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA Storage
 49.1806 -
 49.1807 -
 49.1808 -## IOA-ex
 49.1809 -
 49.1810 -IOA-ex: IOA $(LOG)/IOA-ex.gz
 49.1811 -
 49.1812 -$(LOG)/IOA-ex.gz: $(OUT)/IOA \
 49.1813 -  HOLCF/IOA/ex/ROOT.ML \
 49.1814 -  HOLCF/IOA/ex/TrivEx.thy \
 49.1815 -  HOLCF/IOA/ex/TrivEx2.thy
 49.1816 -	@cd HOLCF/IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ex
 49.1817 -
 49.1818 -
 49.1819 -
 49.1820 -## HOL-Datatype_Benchmark
 49.1821 -
 49.1822 -HOL-Datatype_Benchmark: HOL $(LOG)/HOL-Datatype_Benchmark.gz
 49.1823 -
 49.1824 -$(LOG)/HOL-Datatype_Benchmark.gz: $(OUT)/HOL				\
 49.1825 -  Datatype_Benchmark/ROOT.ML Datatype_Benchmark/Brackin.thy		\
 49.1826 -  Datatype_Benchmark/Instructions.thy Datatype_Benchmark/SML.thy	\
 49.1827 -  Datatype_Benchmark/Verilog.thy
 49.1828 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Datatype_Benchmark
 49.1829 -
 49.1830 -
 49.1831 -## HOL-Record_Benchmark
 49.1832 -
 49.1833 -HOL-Record_Benchmark: HOL $(LOG)/HOL-Record_Benchmark.gz
 49.1834 -
 49.1835 -$(LOG)/HOL-Record_Benchmark.gz: $(OUT)/HOL Record_Benchmark/ROOT.ML	\
 49.1836 -   Record_Benchmark/Record_Benchmark.thy
 49.1837 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Record_Benchmark
 49.1838 -
 49.1839 -
 49.1840 -## HOL-Quickcheck_Benchmark
 49.1841 -
 49.1842 -HOL-Quickcheck_Benchmark: HOL $(LOG)/HOL-Quickcheck_Benchmark.gz
 49.1843 -
 49.1844 -$(LOG)/HOL-Quickcheck_Benchmark.gz: $(OUT)/HOL				\
 49.1845 -  Quickcheck_Benchmark/ROOT.ML						\
 49.1846 -  Quickcheck_Benchmark/Needham_Schroeder_Base.thy			\
 49.1847 -  Quickcheck_Benchmark/Needham_Schroeder_No_Attacker_Example.thy	\
 49.1848 -  Quickcheck_Benchmark/Needham_Schroeder_Guided_Attacker_Example.thy	\
 49.1849 -  Quickcheck_Benchmark/Needham_Schroeder_Unguided_Attacker_Example.thy	\
 49.1850 -  Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy
 49.1851 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quickcheck_Benchmark
 49.1852 -
 49.1853 -
 49.1854 -## clean
 49.1855 -
 49.1856 -clean:
 49.1857 -	@rm -f $(LOG)/HOL-Algebra.gz $(LOG)/HOL-Auth.gz			\
 49.1858 -		$(LOG)/HOL-Bali.gz $(LOG)/HOL-Base.gz			\
 49.1859 -		$(LOG)/HOL-Boogie-Examples.gz $(LOG)/HOL-Boogie.gz	\
 49.1860 -		$(LOG)/HOL-Decision_Procs.gz $(LOG)/HOL-HOL_Light.gz	\
 49.1861 -		$(LOG)/HOL-Hahn_Banach.gz $(LOG)/HOL-Hoare.gz		\
 49.1862 -		$(LOG)/HOL-Hoare_Parallel.gz $(LOG)/HOL-IMP.gz		\
 49.1863 -		$(LOG)/HOL-IMPP.gz $(LOG)/HOL-IOA.gz			\
 49.1864 -		$(LOG)/HOL-Imperative_HOL.gz $(LOG)/HOL-Import.gz	\
 49.1865 -		$(LOG)/HOL-Induct.gz $(LOG)/HOL-Isar_Examples.gz	\
 49.1866 -		$(LOG)/HOL-Lattice $(LOG)/HOL-Lattice.gz		\
 49.1867 -		$(LOG)/HOL-Lex.gz $(LOG)/HOL-Library.gz			\
 49.1868 -		$(LOG)/HOL-Library-Codegenerator_Test.gz		\
 49.1869 -		$(LOG)/HOL-Main.gz $(LOG)/HOL-Matrix_LP.gz		\
 49.1870 -		$(LOG)/HOL-Metis_Examples.gz $(LOG)/HOL-MicroJava.gz	\
 49.1871 -		$(LOG)/HOL-Mirabelle.gz					\
 49.1872 -		$(LOG)/HOL-Multivariate_Analysis.gz			\
 49.1873 -		$(LOG)/HOL-Mutabelle.gz $(LOG)/HOL-NSA-Examples.gz	\
 49.1874 -		$(LOG)/HOL-NSA.gz $(LOG)/HOL-NanoJava.gz		\
 49.1875 -		$(LOG)/HOL-Nitpick_Examples.gz				\
 49.1876 -		$(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-Nominal.gz	\
 49.1877 -		$(LOG)/HOL-Number_Theory.gz				\
 49.1878 -		$(LOG)/HOL-Old_Number_Theory.gz $(LOG)/HOL-Plain.gz	\
 49.1879 -		$(LOG)/HOL-Predicate_Compile_Examples.gz		\
 49.1880 -		$(LOG)/HOL-Probability.gz $(LOG)/HOL-Prolog.gz		\
 49.1881 -		$(LOG)/HOL-Proofs.gz $(LOG)/HOL-Proofs-ex.gz		\
 49.1882 -		$(LOG)/HOL-Proofs-Extraction.gz				\
 49.1883 -		$(LOG)/HOL-Proofs-Lambda.gz				\
 49.1884 -		$(LOG)/HOL-Quickcheck_Examples.gz			\
 49.1885 -		$(LOG)/HOL-Quotient_Examples.gz				\
 49.1886 -		$(LOG)/HOL-SET_Protocol.gz				\
 49.1887 -		$(LOG)/HOL-Word-SMT_Examples.gz $(LOG)/HOL-SPARK.gz	\
 49.1888 -		$(LOG)/HOL-SPARK-Examples.gz				\
 49.1889 -		$(LOG)/HOL-SPARK-Manual.gz $(LOG)/HOL-Statespace.gz	\
 49.1890 -		$(LOG)/HOL-TPTP.gz $(LOG)/HOL-UNITY.gz			\
 49.1891 -		$(LOG)/HOL-Unix.gz $(LOG)/HOL-Word-Examples.gz		\
 49.1892 -		$(LOG)/HOL-Word.gz $(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz	\
 49.1893 -		$(LOG)/HOL.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Inc.gz	\
 49.1894 -		$(LOG)/TLA-Memory.gz $(LOG)/TLA.gz $(OUT)/HOL		\
 49.1895 -		$(OUT)/HOL-Algebra $(OUT)/HOL-Base $(OUT)/HOL-Boogie	\
 49.1896 -		$(OUT)/HOL-HOL_Light $(OUT)/HOL-IMP $(OUT)/HOL-Library	\
 49.1897 -		$(OUT)/HOL-Main $(OUT)/HOL-Multivariate_Analysis	\
 49.1898 -		$(OUT)/HOL-NSA $(OUT)/HOL-Nominal $(OUT)/HOL-Plain	\
 49.1899 -		$(OUT)/HOL-Probability $(OUT)/HOL-Proofs		\
 49.1900 -		$(OUT)/HOL-SPARK $(OUT)/HOL-Word $(OUT)/TLA		\
 49.1901 -		$(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz	\
 49.1902 -		$(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA	\
 49.1903 -		$(LOG)/IOA.gz $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz	\
 49.1904 -		$(LOG)/IOA-Storage.gz $(LOG)/HOLCF-Library.gz		\
 49.1905 -		$(LOG)/IOA-ex.gz $(LOG)/HOLCF-Tutorial.gz		\
 49.1906 -		$(LOG)/HOL-Datatype_Benchmark.gz			\
 49.1907 -		$(LOG)/HOL-Record_Benchmark.gz
    50.1 --- a/src/HOL/Isar_Examples/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    50.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    50.3 @@ -1,21 +0,0 @@
    50.4 -(* Miscellaneous Isabelle/Isar examples for Higher-Order Logic. *)
    50.5 -
    50.6 -no_document use_thys ["~~/src/HOL/Library/Lattice_Syntax", "../Number_Theory/Primes"];
    50.7 -
    50.8 -use_thys [
    50.9 -  "Basic_Logic",
   50.10 -  "Cantor",
   50.11 -  "Drinker",
   50.12 -  "Expr_Compiler",
   50.13 -  "Fibonacci",
   50.14 -  "Group",
   50.15 -  "Group_Context",
   50.16 -  "Group_Notepad",
   50.17 -  "Hoare_Ex",
   50.18 -  "Knaster_Tarski",
   50.19 -  "Mutilated_Checkerboard",
   50.20 -  "Nested_Datatype",
   50.21 -  "Peirce",
   50.22 -  "Puzzle",
   50.23 -  "Summation"
   50.24 -];
    51.1 --- a/src/HOL/Lattice/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    51.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    51.3 @@ -1,7 +0,0 @@
    51.4 -(*  Title:      HOL/Lattice/ROOT.ML
    51.5 -    Author:     Markus Wenzel, TU Muenchen
    51.6 -
    51.7 -Basic theory of lattices and orders.
    51.8 -*)
    51.9 -
   51.10 -use_thys ["CompleteLattice"];
    52.1 --- a/src/HOL/Library/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    52.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    52.3 @@ -1,7 +0,0 @@
    52.4 -
    52.5 -(* Classical Higher-order Logic -- batteries included *)
    52.6 -
    52.7 -use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order",
    52.8 -  "Product_Lattice",
    52.9 -  "Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat"(*, "Code_Prolog"*),
   52.10 -  "Code_Real_Approx_By_Float", "Target_Numeral"];
    53.1 --- a/src/HOL/Matrix_LP/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    53.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    53.3 @@ -1,2 +0,0 @@
    53.4 -
    53.5 -use_thy "Cplex";
    54.1 --- a/src/HOL/Metis_Examples/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    54.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    54.3 @@ -1,9 +0,0 @@
    54.4 -(*  Title:      HOL/Metis_Examples/ROOT.ML
    54.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    54.6 -    Author:     Jasmin Blanchette, TU Muenchen
    54.7 -
    54.8 -Testing Metis and Sledgehammer.
    54.9 -*)
   54.10 -
   54.11 -use_thys ["Abstraction", "Big_O", "Binary_Tree", "Clausification", "Message",
   54.12 -          "Proxies", "Tarski", "Trans_Closure", "Sets"];
    55.1 --- a/src/HOL/MicroJava/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    55.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    55.3 @@ -1,3 +0,0 @@
    55.4 -no_document use_thys ["~~/src/HOL/Library/While_Combinator"];
    55.5 -
    55.6 -use_thys ["MicroJava"];
    56.1 --- a/src/HOL/Mirabelle/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    56.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    56.3 @@ -1,1 +0,0 @@
    56.4 -use_thys ["Mirabelle_Test"];
    57.1 --- a/src/HOL/Multivariate_Analysis/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    57.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    57.3 @@ -1,1 +0,0 @@
    57.4 -use_thys ["Multivariate_Analysis", "Determinants"];
    58.1 --- a/src/HOL/Mutabelle/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    58.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    58.3 @@ -1,3 +0,0 @@
    58.4 -
    58.5 -use_thy "MutabelleExtra";
    58.6 -
    59.1 --- a/src/HOL/NSA/Examples/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    59.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    59.3 @@ -1,1 +0,0 @@
    59.4 -use_thys ["NSPrimes"];
    60.1 --- a/src/HOL/NSA/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    60.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    60.3 @@ -1,1 +0,0 @@
    60.4 -use_thys ["Hypercomplex"];
    61.1 --- a/src/HOL/NanoJava/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    61.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    61.3 @@ -1,1 +0,0 @@
    61.4 -use_thys ["Example"];
    62.1 --- a/src/HOL/Nitpick_Examples/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    62.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    62.3 @@ -1,8 +0,0 @@
    62.4 -(*  Title:      HOL/Nitpick_Examples/ROOT.ML
    62.5 -    Author:     Jasmin Blanchette, TU Muenchen
    62.6 -    Copyright   2009
    62.7 -
    62.8 -Nitpick examples.
    62.9 -*)
   62.10 -
   62.11 -Unsynchronized.setmp quick_and_dirty true use_thys ["Nitpick_Examples"];
    63.1 --- a/src/HOL/Nominal/Examples/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    63.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    63.3 @@ -1,3 +0,0 @@
    63.4 -use_thys ["Nominal_Examples"];
    63.5 -
    63.6 -Unsynchronized.setmp quick_and_dirty true use_thys ["VC_Condition"];
    64.1 --- a/src/HOL/Nominal/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    64.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    64.3 @@ -1,8 +0,0 @@
    64.4 -(*  Title:      HOL/Nominal/ROOT.ML
    64.5 -    Author:     Stefan Berghofer and Christian Urban, TU Muenchen
    64.6 -
    64.7 -The nominal datatype package.
    64.8 -*)
    64.9 -
   64.10 -no_document use_thys ["~~/src/HOL/Library/Infinite_Set"];
   64.11 -use_thys ["Nominal"];
    65.1 --- a/src/HOL/Number_Theory/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    65.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    65.3 @@ -1,1 +0,0 @@
    65.4 -use_thys ["Number_Theory"];
    66.1 --- a/src/HOL/Old_Number_Theory/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    66.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    66.3 @@ -1,15 +0,0 @@
    66.4 -no_document use_thys [
    66.5 -  "~~/src/HOL/Library/Infinite_Set",
    66.6 -  "~~/src/HOL/Library/Permutation"
    66.7 -];
    66.8 -
    66.9 -use_thys [
   66.10 -  "Fib",
   66.11 -  "Factorization",
   66.12 -  "Chinese",
   66.13 -  "WilsonRuss",
   66.14 -  "WilsonBij",
   66.15 -  "Quadratic_Reciprocity",
   66.16 -  "Primes",
   66.17 -  "Pocklington"
   66.18 -];
    67.1 --- a/src/HOL/Predicate_Compile_Examples/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    67.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    67.3 @@ -1,26 +0,0 @@
    67.4 -use_thys [
    67.5 -  "Examples",
    67.6 -  "Predicate_Compile_Tests",
    67.7 -(*  "Predicate_Compile_Quickcheck_Examples", -- should be added again soon *)
    67.8 -  "Specialisation_Examples"
    67.9 -(*  "Hotel_Example_Small_Generator",
   67.10 -  "IMP_1",
   67.11 -  "IMP_2"
   67.12 -  "IMP_3",
   67.13 -  "IMP_4"*)];
   67.14 -
   67.15 -if getenv "ISABELLE_SWIPL" = "" andalso getenv "ISABELLE_YAP" = "" then
   67.16 -  (warning "No prolog system found - skipping some example theories"; ())
   67.17 -else
   67.18 -  if not (getenv "ISABELLE_SWIPL" = "") orelse
   67.19 -    #1 (Isabelle_System.bash_output "\"$ISABELLE_PREDICATE_COMPILE/lib/scripts/swipl_version\"") =
   67.20 -      "5.10.1"
   67.21 -  then
   67.22 -     (use_thys [
   67.23 -        "Code_Prolog_Examples",
   67.24 -        "Context_Free_Grammar_Example",
   67.25 -        "Hotel_Example_Prolog",
   67.26 -        "Lambda_Example",
   67.27 -        "List_Examples"];
   67.28 -      Unsynchronized.setmp quick_and_dirty true use_thys ["Reg_Exp_Example"])
   67.29 -  else (warning "Unsupported SWI-Prolog version - skipping some example theories"; ());
    68.1 --- a/src/HOL/Probability/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    68.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    68.3 @@ -1,9 +0,0 @@
    68.4 -no_document use_thys [
    68.5 -  "~~/src/HOL/Library/Countable",
    68.6 -  "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits",
    68.7 -  "~~/src/HOL/Library/Permutation"];
    68.8 -
    68.9 -use_thys [
   68.10 -  "Probability",
   68.11 -  "ex/Dining_Cryptographers",
   68.12 -  "ex/Koepf_Duermuth_Countermeasure" ];
    69.1 --- a/src/HOL/Prolog/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    69.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    69.3 @@ -1,5 +0,0 @@
    69.4 -(*  Title:    HOL/Prolog/ROOT.ML
    69.5 -    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
    69.6 -*)
    69.7 -
    69.8 -use_thys ["Test", "Type"];
    70.1 --- a/src/HOL/Proofs/Extraction/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    70.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    70.3 @@ -1,11 +0,0 @@
    70.4 -(* Examples for program extraction in Higher-Order Logic *)
    70.5 -
    70.6 -no_document use_thys [
    70.7 -  "~~/src/HOL/Library/Efficient_Nat",
    70.8 -  "~~/src/HOL/Library/Monad_Syntax",
    70.9 -  "~~/src/HOL/Number_Theory/Primes",
   70.10 -  "~~/src/HOL/Number_Theory/UniqueFactorization",
   70.11 -  "~~/src/HOL/Library/State_Monad"
   70.12 -];
   70.13 -
   70.14 -use_thys ["Greatest_Common_Divisor", "Warshall", "Higman_Extraction", "Pigeonhole", "Euclid"];
    71.1 --- a/src/HOL/Proofs/Lambda/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    71.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    71.3 @@ -1,2 +0,0 @@
    71.4 -no_document use_thys ["~~/src/HOL/Library/Code_Integer"];
    71.5 -use_thys ["Eta", "StrongNorm", "Standardization", "WeakNorm"];
    72.1 --- a/src/HOL/Proofs/ex/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    72.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    72.3 @@ -1,1 +0,0 @@
    72.4 -use_thys ["Hilbert_Classical"];
    73.1 --- a/src/HOL/Quickcheck_Benchmark/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    73.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    73.3 @@ -1,6 +0,0 @@
    73.4 -Unsynchronized.setmp quick_and_dirty true use_thys [
    73.5 -  "Find_Unused_Assms_Examples",
    73.6 -  "Needham_Schroeder_No_Attacker_Example",
    73.7 -  "Needham_Schroeder_Guided_Attacker_Example",
    73.8 -  "Needham_Schroeder_Unguided_Attacker_Example"
    73.9 -]
    74.1 --- a/src/HOL/Quickcheck_Examples/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    74.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    74.3 @@ -1,12 +0,0 @@
    74.4 -use_thys [
    74.5 -  "Quickcheck_Examples"
    74.6 -  (*,
    74.7 -  "Quickcheck_Lattice_Examples",
    74.8 -  "Completeness",
    74.9 -  "Quickcheck_Interfaces",
   74.10 -  "Hotel_Example",*)
   74.11 -];
   74.12 -
   74.13 -if getenv "ISABELLE_GHC" = "" then ()
   74.14 -else use_thy "Quickcheck_Narrowing_Examples";
   74.15 -
    75.1 --- a/src/HOL/Quotient_Examples/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    75.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    75.3 @@ -1,9 +0,0 @@
    75.4 -(*  Title:      HOL/Quotient_Examples/ROOT.ML
    75.5 -    Author:     Cezary Kaliszyk and Christian Urban
    75.6 -
    75.7 -Testing the quotient package.
    75.8 -*)
    75.9 -
   75.10 -use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Lift_FSet",
   75.11 -  "Lift_Set", "Lift_Fun", "Quotient_Rat", "Lift_DList"];
   75.12 -
    76.1 --- a/src/HOL/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    76.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    76.3 @@ -1,4 +0,0 @@
    76.4 -
    76.5 -(* Classical Higher-order Logic *)
    76.6 -
    76.7 -use_thys ["Complex_Main"];
    77.1 --- a/src/HOL/Record_Benchmark/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    77.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    77.3 @@ -1,8 +0,0 @@
    77.4 -(*  Title:      HOL/Record_Benchmark/ROOT.ML
    77.5 -
    77.6 -Some benchmark on large record.
    77.7 -*)
    77.8 -
    77.9 -Toplevel.timing := true;
   77.10 -
   77.11 -use_thys ["Record_Benchmark"];
    78.1 --- a/src/HOL/SET_Protocol/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    78.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    78.3 @@ -1,2 +0,0 @@
    78.4 -no_document use_thys ["~~/src/HOL/Library/Nat_Bijection"];
    78.5 -use_thys ["SET_Protocol"];
    79.1 --- a/src/HOL/SMT_Examples/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    79.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    79.3 @@ -1,2 +0,0 @@
    79.4 -quick_and_dirty := true;
    79.5 -use_thys ["SMT_Tests", "SMT_Examples", "SMT_Word_Examples"];
    80.1 --- a/src/HOL/SPARK/Examples/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    80.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    80.3 @@ -1,16 +0,0 @@
    80.4 -use_thys
    80.5 -  ["Gcd/Greatest_Common_Divisor",
    80.6 -
    80.7 -   "Liseq/Longest_Increasing_Subsequence",
    80.8 -
    80.9 -   "RIPEMD-160/F",
   80.10 -   "RIPEMD-160/Hash",
   80.11 -   "RIPEMD-160/K_L",
   80.12 -   "RIPEMD-160/K_R",
   80.13 -   "RIPEMD-160/R_L",
   80.14 -   "RIPEMD-160/Round",
   80.15 -   "RIPEMD-160/R_R",
   80.16 -   "RIPEMD-160/S_L",
   80.17 -   "RIPEMD-160/S_R",
   80.18 -
   80.19 -   "Sqrt/Sqrt"];
    81.1 --- a/src/HOL/SPARK/Manual/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    81.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    81.3 @@ -1,7 +0,0 @@
    81.4 -Printer.show_question_marks_default := false;
    81.5 -
    81.6 -use_thys
    81.7 -  ["Example_Verification",
    81.8 -   "VC_Principles",
    81.9 -   "Reference",
   81.10 -   "Complex_Types"];
    82.1 --- a/src/HOL/SPARK/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    82.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    82.3 @@ -1,1 +0,0 @@
    82.4 -use_thys ["SPARK"];
    83.1 --- a/src/HOL/Statespace/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    83.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    83.3 @@ -1,1 +0,0 @@
    83.4 -use_thys ["StateSpaceEx"];
    84.1 --- a/src/HOL/TLA/Buffer/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    84.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    84.3 @@ -1,1 +0,0 @@
    84.4 -use_thys ["DBuffer"];
    85.1 --- a/src/HOL/TLA/Inc/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    85.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    85.3 @@ -1,1 +0,0 @@
    85.4 -use_thys ["Inc"];
    86.1 --- a/src/HOL/TLA/Memory/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    86.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    86.3 @@ -1,1 +0,0 @@
    86.4 -use_thys ["MemoryImplementation"];
    87.1 --- a/src/HOL/TLA/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    87.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    87.3 @@ -1,3 +0,0 @@
    87.4 -(* The Temporal Logic of Actions *)
    87.5 -
    87.6 -use_thys ["TLA"];
    88.1 --- a/src/HOL/TPTP/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    88.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    88.3 @@ -1,18 +0,0 @@
    88.4 -(*  Title:      HOL/TPTP/ROOT.ML
    88.5 -    Author:     Jasmin Blanchette, TU Muenchen
    88.6 -    Author:     Nik Sultana, University of Cambridge
    88.7 -    Copyright   2011
    88.8 -
    88.9 -TPTP-related extensions.
   88.10 -*)
   88.11 -
   88.12 -use_thys [
   88.13 -  "ATP_Theory_Export",
   88.14 -  "MaSh_Eval",
   88.15 -  "MaSh_Export",
   88.16 -  "TPTP_Interpret",
   88.17 -  "THF_Arith"
   88.18 -];
   88.19 -
   88.20 -Unsynchronized.setmp Proofterm.proofs (!Proofterm.proofs)
   88.21 -  use_thy "ATP_Problem_Import";
    89.1 --- a/src/HOL/UNITY/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    89.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    89.3 @@ -1,43 +0,0 @@
    89.4 -(*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    89.5 -    Copyright   1998  University of Cambridge
    89.6 -*)
    89.7 -
    89.8 -(*Verifying security protocols using UNITY*)
    89.9 -no_document use_thys ["../Auth/Public"];
   89.10 -
   89.11 -use_thys [
   89.12 -  (*Basic meta-theory*)
   89.13 -  "UNITY_Main",
   89.14 -
   89.15 -  (*Simple examples: no composition*)
   89.16 -  "Simple/Deadlock",
   89.17 -  "Simple/Common",
   89.18 -  "Simple/Network",
   89.19 -  "Simple/Token",
   89.20 -  "Simple/Channel",
   89.21 -  "Simple/Lift",
   89.22 -  "Simple/Mutex",
   89.23 -  "Simple/Reach",
   89.24 -  "Simple/Reachability",
   89.25 -
   89.26 -  (*Verifying security protocols using UNITY*)
   89.27 -  "Simple/NSP_Bad",
   89.28 -
   89.29 -  (*Example of composition*)
   89.30 -  "Comp/Handshake",
   89.31 -
   89.32 -  (*Universal properties examples*)
   89.33 -  "Comp/Counter",
   89.34 -  "Comp/Counterc",
   89.35 -  "Comp/Priority",
   89.36 -
   89.37 -  "Comp/TimerArray",
   89.38 -  "Comp/Progress",
   89.39 -
   89.40 -  "Comp/Alloc",
   89.41 -  "Comp/AllocImpl",
   89.42 -  "Comp/Client",
   89.43 -
   89.44 -  (*obsolete*)
   89.45 -  "ELT"
   89.46 -];
    90.1 --- a/src/HOL/Unix/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    90.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    90.3 @@ -1,1 +0,0 @@
    90.4 -use_thys ["Unix"];
    91.1 --- a/src/HOL/Word/Examples/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    91.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    91.3 @@ -1,1 +0,0 @@
    91.4 -use_thys ["WordExamples"];
    92.1 --- a/src/HOL/Word/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    92.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    92.3 @@ -1,1 +0,0 @@
    92.4 -use_thys ["Word"];
    93.1 --- a/src/HOL/ZF/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    93.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    93.3 @@ -1,1 +0,0 @@
    93.4 -use_thys ["MainZF", "Games"];
    94.1 --- a/src/HOL/ex/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    94.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    94.3 @@ -1,90 +0,0 @@
    94.4 -(*  Title:      HOL/ex/ROOT.ML
    94.5 -
    94.6 -Miscellaneous examples for Higher-Order Logic.
    94.7 -*)
    94.8 -
    94.9 -no_document use_thys [
   94.10 -  "~~/src/HOL/Library/State_Monad",
   94.11 -  "Code_Nat_examples",
   94.12 -  "~~/src/HOL/Library/FuncSet",
   94.13 -  "Eval_Examples",
   94.14 -  "Normalization_by_Evaluation",
   94.15 -  "Hebrew",
   94.16 -  "Chinese",
   94.17 -  "Serbian",
   94.18 -  "~~/src/HOL/Library/FinFun_Syntax"
   94.19 -];
   94.20 -
   94.21 -use_thys [
   94.22 -  "Iff_Oracle",
   94.23 -  "Coercion_Examples",
   94.24 -  "Numeral_Representation",
   94.25 -  "Higher_Order_Logic",
   94.26 -  "Abstract_NAT",
   94.27 -  "Guess",
   94.28 -  "Binary",
   94.29 -  "Fundefs",
   94.30 -  "Induction_Schema",
   94.31 -  "LocaleTest2",
   94.32 -  "Records",
   94.33 -  "While_Combinator_Example",
   94.34 -  "MonoidGroup",
   94.35 -  "BinEx",
   94.36 -  "Hex_Bin_Examples",
   94.37 -  "Antiquote",
   94.38 -  "Multiquote",
   94.39 -  "PER",
   94.40 -  "NatSum",
   94.41 -  "ThreeDivides",
   94.42 -  "Intuitionistic",
   94.43 -  "CTL",
   94.44 -  "Arith_Examples",
   94.45 -  "BT",
   94.46 -  "Tree23",
   94.47 -  "MergeSort",
   94.48 -  "Lagrange",
   94.49 -  "Groebner_Examples",
   94.50 -  "MT",
   94.51 -  "Unification",
   94.52 -  "Primrec",
   94.53 -  "Tarski",
   94.54 -  "Classical",
   94.55 -  "Set_Theory",
   94.56 -  "Meson_Test",
   94.57 -  "Termination",
   94.58 -  "Coherent",
   94.59 -  "PresburgerEx",
   94.60 -  "ReflectionEx",
   94.61 -  "Sqrt",
   94.62 -  "Sqrt_Script",
   94.63 -  "Transfer_Ex",
   94.64 -  "Transfer_Int_Nat",
   94.65 -  "HarmonicSeries",
   94.66 -  "Refute_Examples",
   94.67 -  "Landau",
   94.68 -  "Execute_Choice",
   94.69 -  "Summation",
   94.70 -  "Gauge_Integration",
   94.71 -  "Dedekind_Real",
   94.72 -  "Quicksort",
   94.73 -  "Birthday_Paradox",
   94.74 -  "List_to_Set_Comprehension_Examples",
   94.75 -  "Seq",
   94.76 -  "Simproc_Tests",
   94.77 -  "Executable_Relation",
   94.78 -  "FinFunPred",
   94.79 -  "Set_Comprehension_Pointfree_Tests",
   94.80 -  "Parallel_Example"
   94.81 -];
   94.82 -
   94.83 -use_thy "SVC_Oracle";
   94.84 -if getenv "SVC_HOME" = "" then ()
   94.85 -else use_thy "svc_test";
   94.86 -
   94.87 -(*requires zChaff (or some other reasonably fast SAT solver)*)
   94.88 -if getenv "ZCHAFF_HOME" = "" then ()
   94.89 -else use_thy "Sudoku";
   94.90 -
   94.91 -(*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
   94.92 -(*global side-effects ahead!*)
   94.93 -try use_thy "SAT_Examples";   (* FIXME try!? (not really a proper test) *)
    95.1 --- a/src/LCF/IsaMakefile	Tue Aug 07 23:38:18 2012 +0200
    95.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    95.3 @@ -1,44 +0,0 @@
    95.4 -#
    95.5 -# IsaMakefile for LCF
    95.6 -#
    95.7 -
    95.8 -## targets
    95.9 -
   95.10 -default: LCF
   95.11 -images: LCF
   95.12 -test: LCF-ex
   95.13 -all: images test
   95.14 -full: all
   95.15 -smlnj: all
   95.16 -
   95.17 -
   95.18 -## global settings
   95.19 -
   95.20 -SRC = $(ISABELLE_HOME)/src
   95.21 -OUT = $(ISABELLE_OUTPUT)
   95.22 -LOG = $(OUT)/log
   95.23 -
   95.24 -
   95.25 -## LCF
   95.26 -
   95.27 -LCF: FOL $(OUT)/LCF
   95.28 -
   95.29 -FOL:
   95.30 -	@cd $(SRC)/FOL; $(ISABELLE_TOOL) make FOL
   95.31 -
   95.32 -$(OUT)/LCF: $(OUT)/FOL LCF.thy ROOT.ML
   95.33 -	@$(ISABELLE_TOOL) usedir -b -r $(OUT)/FOL LCF
   95.34 -
   95.35 -
   95.36 -## LCF-ex
   95.37 -
   95.38 -LCF-ex: LCF $(LOG)/LCF-ex.gz
   95.39 -
   95.40 -$(LOG)/LCF-ex.gz: $(OUT)/LCF ex/Ex1.thy ex/Ex2.thy ex/Ex3.thy ex/Ex4.thy ex/ROOT.ML
   95.41 -	@$(ISABELLE_TOOL) usedir $(OUT)/LCF ex
   95.42 -
   95.43 -
   95.44 -## clean
   95.45 -
   95.46 -clean:
   95.47 -	@rm -f $(OUT)/LCF $(LOG)/LCF.gz $(LOG)/LCF-ex.gz
    96.1 --- a/src/LCF/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    96.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    96.3 @@ -1,7 +0,0 @@
    96.4 -(*  Title:      LCF/ROOT.ML
    96.5 -    Author:     Tobias Nipkow
    96.6 -    Copyright   1992  University of Cambridge
    96.7 -*)
    96.8 -
    96.9 -use_thys ["LCF"];
   96.10 -
    97.1 --- a/src/LCF/ex/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
    97.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    97.3 @@ -1,8 +0,0 @@
    97.4 -(*  Title:      LCF/ex/ROOT.ML
    97.5 -    Author:     Tobias Nipkow
    97.6 -    Copyright   1991  University of Cambridge
    97.7 -
    97.8 -Some examples from Lawrence Paulson's book Logic and Computation.
    97.9 -*)
   97.10 -
   97.11 -use_thys ["Ex1", "Ex2", "Ex3", "Ex4"];
    98.1 --- a/src/Pure/IsaMakefile	Tue Aug 07 23:38:18 2012 +0200
    98.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    98.3 @@ -1,270 +0,0 @@
    98.4 -#
    98.5 -# IsaMakefile for Pure
    98.6 -#
    98.7 -
    98.8 -## targets
    98.9 -
   98.10 -default: Pure
   98.11 -images: Pure
   98.12 -test: RAW
   98.13 -all: images test
   98.14 -full: all
   98.15 -smlnj: all
   98.16 -
   98.17 -
   98.18 -## global settings
   98.19 -
   98.20 -SRC = $(ISABELLE_HOME)/src
   98.21 -OUT = $(ISABELLE_OUTPUT)
   98.22 -LOG = $(OUT)/log
   98.23 -
   98.24 -
   98.25 -## Pure
   98.26 -
   98.27 -BOOTSTRAP_FILES = 					\
   98.28 -  General/exn.ML					\
   98.29 -  ML-Systems/compiler_polyml.ML			\
   98.30 -  ML-Systems/ml_name_space.ML				\
   98.31 -  ML-Systems/ml_pretty.ML				\
   98.32 -  ML-Systems/ml_system.ML				\
   98.33 -  ML-Systems/multithreading.ML				\
   98.34 -  ML-Systems/multithreading_polyml.ML			\
   98.35 -  ML-Systems/overloading_smlnj.ML			\
   98.36 -  ML-Systems/polyml.ML					\
   98.37 -  ML-Systems/pp_dummy.ML				\
   98.38 -  ML-Systems/proper_int.ML				\
   98.39 -  ML-Systems/single_assignment.ML			\
   98.40 -  ML-Systems/single_assignment_polyml.ML		\
   98.41 -  ML-Systems/smlnj.ML					\
   98.42 -  ML-Systems/thread_dummy.ML				\
   98.43 -  ML-Systems/universal.ML				\
   98.44 -  ML-Systems/unsynchronized.ML				\
   98.45 -  ML-Systems/use_context.ML
   98.46 -
   98.47 -RAW: $(OUT)/RAW
   98.48 -
   98.49 -$(OUT)/RAW: $(BOOTSTRAP_FILES)
   98.50 -	@./mk -r
   98.51 -
   98.52 -
   98.53 -Pure: $(OUT)/Pure
   98.54 -
   98.55 -$(OUT)/Pure: $(BOOTSTRAP_FILES)				\
   98.56 -  Concurrent/bash.ML 					\
   98.57 -  Concurrent/bash_sequential.ML				\
   98.58 -  Concurrent/cache.ML					\
   98.59 -  Concurrent/future.ML					\
   98.60 -  Concurrent/lazy.ML					\
   98.61 -  Concurrent/lazy_sequential.ML				\
   98.62 -  Concurrent/mailbox.ML					\
   98.63 -  Concurrent/par_exn.ML					\
   98.64 -  Concurrent/par_list.ML				\
   98.65 -  Concurrent/par_list_sequential.ML			\
   98.66 -  Concurrent/simple_thread.ML				\
   98.67 -  Concurrent/single_assignment.ML			\
   98.68 -  Concurrent/single_assignment_sequential.ML		\
   98.69 -  Concurrent/synchronized.ML				\
   98.70 -  Concurrent/synchronized_sequential.ML			\
   98.71 -  Concurrent/task_queue.ML				\
   98.72 -  Concurrent/time_limit.ML				\
   98.73 -  General/alist.ML					\
   98.74 -  General/antiquote.ML					\
   98.75 -  General/balanced_tree.ML				\
   98.76 -  General/basics.ML					\
   98.77 -  General/binding.ML					\
   98.78 -  General/buffer.ML					\
   98.79 -  General/file.ML					\
   98.80 -  General/graph.ML					\
   98.81 -  General/heap.ML					\
   98.82 -  General/integer.ML					\
   98.83 -  General/linear_set.ML					\
   98.84 -  General/long_name.ML					\
   98.85 -  General/name_space.ML					\
   98.86 -  General/ord_list.ML					\
   98.87 -  General/output.ML					\
   98.88 -  General/path.ML					\
   98.89 -  General/position.ML					\
   98.90 -  General/pretty.ML					\
   98.91 -  General/print_mode.ML					\
   98.92 -  General/properties.ML					\
   98.93 -  General/queue.ML					\
   98.94 -  General/same.ML					\
   98.95 -  General/scan.ML					\
   98.96 -  General/secure.ML					\
   98.97 -  General/seq.ML					\
   98.98 -  General/sha1.ML					\
   98.99 -  General/sha1_polyml.ML				\
  98.100 -  General/source.ML					\
  98.101 -  General/stack.ML					\
  98.102 -  General/symbol.ML					\
  98.103 -  General/symbol_pos.ML					\
  98.104 -  General/table.ML					\
  98.105 -  General/timing.ML					\
  98.106 -  General/url.ML					\
  98.107 -  Isar/args.ML						\
  98.108 -  Isar/attrib.ML					\
  98.109 -  Isar/auto_bind.ML					\
  98.110 -  Isar/bundle.ML					\
  98.111 -  Isar/calculation.ML					\
  98.112 -  Isar/class.ML						\
  98.113 -  Isar/class_declaration.ML				\
  98.114 -  Isar/code.ML						\
  98.115 -  Isar/context_rules.ML					\
  98.116 -  Isar/element.ML					\
  98.117 -  Isar/expression.ML					\
  98.118 -  Isar/generic_target.ML				\
  98.119 -  Isar/isar_cmd.ML					\
  98.120 -  Isar/isar_syn.ML					\
  98.121 -  Isar/keyword.ML					\
  98.122 -  Isar/local_defs.ML					\
  98.123 -  Isar/local_theory.ML					\
  98.124 -  Isar/locale.ML					\
  98.125 -  Isar/method.ML					\
  98.126 -  Isar/named_target.ML					\
  98.127 -  Isar/object_logic.ML					\
  98.128 -  Isar/obtain.ML					\
  98.129 -  Isar/outer_syntax.ML					\
  98.130 -  Isar/overloading.ML					\
  98.131 -  Isar/parse.ML						\
  98.132 -  Isar/parse_spec.ML					\
  98.133 -  Isar/proof.ML						\
  98.134 -  Isar/proof_context.ML					\
  98.135 -  Isar/proof_display.ML					\
  98.136 -  Isar/proof_node.ML					\
  98.137 -  Isar/rule_cases.ML					\
  98.138 -  Isar/rule_insts.ML					\
  98.139 -  Isar/runtime.ML					\
  98.140 -  Isar/skip_proof.ML					\
  98.141 -  Isar/spec_rules.ML					\
  98.142 -  Isar/specification.ML					\
  98.143 -  Isar/token.ML						\
  98.144 -  Isar/toplevel.ML					\
  98.145 -  Isar/typedecl.ML					\
  98.146 -  ML/install_pp_polyml.ML				\
  98.147 -  ML/ml_antiquote.ML					\
  98.148 -  ML/ml_compiler.ML					\
  98.149 -  ML/ml_compiler_polyml.ML				\
  98.150 -  ML/ml_context.ML					\
  98.151 -  ML/ml_env.ML						\
  98.152 -  ML/ml_lex.ML						\
  98.153 -  ML/ml_parse.ML					\
  98.154 -  ML/ml_syntax.ML					\
  98.155 -  ML/ml_thms.ML						\
  98.156 -  PIDE/command.ML					\
  98.157 -  PIDE/document.ML					\
  98.158 -  PIDE/isabelle_markup.ML				\
  98.159 -  PIDE/markup.ML					\
  98.160 -  PIDE/protocol.ML					\
  98.161 -  PIDE/xml.ML						\
  98.162 -  PIDE/yxml.ML						\
  98.163 -  Proof/extraction.ML					\
  98.164 -  Proof/proof_checker.ML				\
  98.165 -  Proof/proof_rewrite_rules.ML				\
  98.166 -  Proof/proof_syntax.ML					\
  98.167 -  Proof/reconstruct.ML					\
  98.168 -  ProofGeneral/pgip.ML					\
  98.169 -  ProofGeneral/pgip_input.ML				\
  98.170 -  ProofGeneral/pgip_isabelle.ML				\
  98.171 -  ProofGeneral/pgip_markup.ML				\
  98.172 -  ProofGeneral/pgip_output.ML				\
  98.173 -  ProofGeneral/pgip_parser.ML				\
  98.174 -  ProofGeneral/pgip_tests.ML				\
  98.175 -  ProofGeneral/pgip_types.ML				\
  98.176 -  ProofGeneral/pgml.ML					\
  98.177 -  ProofGeneral/preferences.ML				\
  98.178 -  ProofGeneral/proof_general_emacs.ML			\
  98.179 -  ProofGeneral/proof_general_pgip.ML			\
  98.180 -  Pure.thy						\
  98.181 -  ROOT.ML						\
  98.182 -  Syntax/ast.ML						\
  98.183 -  Syntax/lexicon.ML					\
  98.184 -  Syntax/local_syntax.ML				\
  98.185 -  Syntax/mixfix.ML					\
  98.186 -  Syntax/parser.ML					\
  98.187 -  Syntax/printer.ML					\
  98.188 -  Syntax/simple_syntax.ML				\
  98.189 -  Syntax/syntax.ML					\
  98.190 -  Syntax/syntax_ext.ML					\
  98.191 -  Syntax/syntax_phases.ML				\
  98.192 -  Syntax/syntax_trans.ML				\
  98.193 -  Syntax/term_position.ML				\
  98.194 -  System/build.ML					\
  98.195 -  System/command_line.ML				\
  98.196 -  System/invoke_scala.ML				\
  98.197 -  System/isabelle_process.ML				\
  98.198 -  System/isabelle_system.ML				\
  98.199 -  System/isar.ML					\
  98.200 -  System/options.ML					\
  98.201 -  System/session.ML					\
  98.202 -  System/system_channel.ML				\
  98.203 -  Thy/html.ML						\
  98.204 -  Thy/latex.ML						\
  98.205 -  Thy/present.ML					\
  98.206 -  Thy/rail.ML						\
  98.207 -  Thy/term_style.ML					\
  98.208 -  Thy/thm_deps.ML					\
  98.209 -  Thy/thy_header.ML					\
  98.210 -  Thy/thy_info.ML					\
  98.211 -  Thy/thy_load.ML					\
  98.212 -  Thy/thy_output.ML					\
  98.213 -  Thy/thy_syntax.ML					\
  98.214 -  Tools/find_consts.ML					\
  98.215 -  Tools/find_theorems.ML				\
  98.216 -  Tools/named_thms.ML					\
  98.217 -  Tools/xml_syntax.ML					\
  98.218 -  assumption.ML						\
  98.219 -  axclass.ML						\
  98.220 -  config.ML						\
  98.221 -  conjunction.ML					\
  98.222 -  consts.ML						\
  98.223 -  context.ML						\
  98.224 -  context_position.ML					\
  98.225 -  conv.ML						\
  98.226 -  defs.ML						\
  98.227 -  display.ML						\
  98.228 -  drule.ML						\
  98.229 -  envir.ML						\
  98.230 -  facts.ML						\
  98.231 -  global_theory.ML					\
  98.232 -  goal.ML						\
  98.233 -  goal_display.ML					\
  98.234 -  interpretation.ML					\
  98.235 -  item_net.ML						\
  98.236 -  library.ML						\
  98.237 -  logic.ML						\
  98.238 -  more_thm.ML						\
  98.239 -  morphism.ML						\
  98.240 -  name.ML						\
  98.241 -  net.ML						\
  98.242 -  pattern.ML						\
  98.243 -  primitive_defs.ML					\
  98.244 -  proofterm.ML						\
  98.245 -  pure_setup.ML						\
  98.246 -  pure_thy.ML						\
  98.247 -  raw_simplifier.ML					\
  98.248 -  search.ML						\
  98.249 -  sign.ML						\
  98.250 -  simplifier.ML						\
  98.251 -  sorts.ML						\
  98.252 -  subgoal.ML						\
  98.253 -  tactic.ML						\
  98.254 -  tactical.ML						\
  98.255 -  term.ML						\
  98.256 -  term_ord.ML						\
  98.257 -  term_sharing.ML					\
  98.258 -  term_subst.ML						\
  98.259 -  term_xml.ML						\
  98.260 -  theory.ML						\
  98.261 -  thm.ML						\
  98.262 -  type.ML						\
  98.263 -  type_infer.ML						\
  98.264 -  type_infer_context.ML					\
  98.265 -  unify.ML						\
  98.266 -  variable.ML
  98.267 -	@./mk
  98.268 -
  98.269 -
  98.270 -## clean
  98.271 -
  98.272 -clean:
  98.273 -	@rm -f $(OUT)/Pure $(LOG)/Pure.gz $(OUT)/RAW $(LOG)/RAW.gz
    99.1 --- a/src/Sequents/IsaMakefile	Tue Aug 07 23:38:18 2012 +0200
    99.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    99.3 @@ -1,47 +0,0 @@
    99.4 -#
    99.5 -# IsaMakefile for Sequents
    99.6 -#
    99.7 -
    99.8 -## targets
    99.9 -
   99.10 -default: Sequents
   99.11 -images: Sequents
   99.12 -test: Sequents-LK
   99.13 -all: images test
   99.14 -full: all
   99.15 -smlnj: all
   99.16 -
   99.17 -
   99.18 -## global settings
   99.19 -
   99.20 -SRC = $(ISABELLE_HOME)/src
   99.21 -OUT = $(ISABELLE_OUTPUT)
   99.22 -LOG = $(OUT)/log
   99.23 -
   99.24 -
   99.25 -## Sequents
   99.26 -
   99.27 -Sequents: Pure $(OUT)/Sequents
   99.28 -
   99.29 -Pure:
   99.30 -	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
   99.31 -
   99.32 -$(OUT)/Sequents: $(OUT)/Pure ILL.thy LK0.thy LK.thy \
   99.33 -  modal.ML ROOT.ML simpdata.ML S4.thy S43.thy Sequents.thy T.thy prover.ML \
   99.34 -  ILL_predlog.thy Washing.thy
   99.35 -	@$(ISABELLE_TOOL) usedir -b $(OUT)/Pure Sequents
   99.36 -
   99.37 -
   99.38 -## Sequents-LK
   99.39 -
   99.40 -Sequents-LK: Sequents $(LOG)/Sequents-LK.gz
   99.41 -
   99.42 -$(LOG)/Sequents-LK.gz: $(OUT)/Sequents LK/ROOT.ML LK/Hard_Quantifiers.thy \
   99.43 -  LK/Propositional.thy LK/Quantifiers.thy LK/Nat.thy
   99.44 -	@$(ISABELLE_TOOL) usedir $(OUT)/Sequents LK
   99.45 -
   99.46 -
   99.47 -## clean
   99.48 -
   99.49 -clean:
   99.50 -	@rm -f $(OUT)/Sequents $(LOG)/Sequents.gz $(LOG)/Sequents-LK.gz
   100.1 --- a/src/Sequents/LK/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
   100.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
   100.3 @@ -1,9 +0,0 @@
   100.4 -(*  Title:      Sequents/LK/ROOT.ML
   100.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   100.6 -    Copyright   1992  University of Cambridge
   100.7 -
   100.8 -Examples for Classical Logic.
   100.9 -*)
  100.10 -
  100.11 -use_thys ["Propositional", "Quantifiers", "Hard_Quantifiers", "Nat"];
  100.12 -
   101.1 --- a/src/Sequents/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
   101.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
   101.3 @@ -1,8 +0,0 @@
   101.4 -(*  Title:      Sequents/ROOT.ML
   101.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   101.6 -    Copyright   1991  University of Cambridge
   101.7 -
   101.8 -Classical Sequent Calculus based on Pure Isabelle. 
   101.9 -*)
  101.10 -
  101.11 -use_thys ["LK", "ILL", "ILL_predlog", "Washing", "Modal0", "T", "S4", "S43"];
   102.1 --- a/src/Tools/WWW_Find/IsaMakefile	Tue Aug 07 23:38:18 2012 +0200
   102.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
   102.3 @@ -1,42 +0,0 @@
   102.4 -#
   102.5 -# IsaMakefile for WWW_Find
   102.6 -#
   102.7 -# Provides static compile check for ML files only.
   102.8 -
   102.9 -## targets
  102.10 -
  102.11 -default: Pure-WWW_Find
  102.12 -images:
  102.13 -test: Pure-WWW_Find
  102.14 -all: images test
  102.15 -full: all
  102.16 -smlnj: all
  102.17 -
  102.18 -
  102.19 -## global settings
  102.20 -
  102.21 -SRC = $(ISABELLE_HOME)/src
  102.22 -OUT = $(ISABELLE_OUTPUT)
  102.23 -LOG = $(OUT)/log
  102.24 -
  102.25 -
  102.26 -## Pure-WWW_Find
  102.27 -
  102.28 -LOGFILE = $(LOG)/Pure-WWW_Find.gz
  102.29 -
  102.30 -Pure-WWW_Find: Pure $(LOGFILE)
  102.31 -
  102.32 -Pure:
  102.33 -	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
  102.34 -
  102.35 -$(LOGFILE): $(OUT)/Pure echo.ML find_theorems.ML html_unicode.ML	\
  102.36 -  html_templates.ML http_status.ML http_util.ML mime.ML scgi_req.ML	\
  102.37 -  scgi_server.ML socket_util.ML unicode_symbols.ML xhtml.ML		\
  102.38 -  yxml_find_theorems.ML ROOT.ML
  102.39 -	@cd ..; $(ISABELLE_TOOL) usedir Pure WWW_Find
  102.40 -
  102.41 -
  102.42 -## clean
  102.43 -
  102.44 -clean:
  102.45 -	@rm -f $(LOGFILE)
   103.1 --- a/src/Tools/WWW_Find/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
   103.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
   103.3 @@ -1,3 +0,0 @@
   103.4 -if ML_System.is_polyml then use_thy "WWW_Find"
   103.5 -else ();
   103.6 -
   104.1 --- a/src/ZF/AC/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
   104.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
   104.3 @@ -1,9 +0,0 @@
   104.4 -(*  Title:      ZF/AC/ROOT.ML
   104.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   104.6 -    Copyright   1995  University of Cambridge
   104.7 -
   104.8 -Proofs of AC-equivalences, due to Krzysztof Grabczewski.
   104.9 -*)
  104.10 -
  104.11 -use_thys ["WO6_WO1", "WO1_WO7", "AC7_AC9", "WO1_AC", "AC15_WO6",
  104.12 -  "WO2_AC16", "AC16_WO4", "AC17_AC1", "AC18_AC19", "DC"];
   105.1 --- a/src/ZF/Coind/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
   105.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
   105.3 @@ -1,15 +0,0 @@
   105.4 -(*  Title:      ZF/Coind/ROOT.ML
   105.5 -    Author:     Jacob Frost, Cambridge University Computer Laboratory
   105.6 -    Copyright   1995  University of Cambridge
   105.7 -
   105.8 -Based upon the article
   105.9 -    Robin Milner and Mads Tofte,
  105.10 -    Co-induction in Relational Semantics,
  105.11 -    Theoretical Computer Science 87 (1991), pages 209-220.
  105.12 -
  105.13 -Written up as
  105.14 -    Jacob Frost, A Case Study of Co_induction in Isabelle
  105.15 -    Report, Computer Lab, University of Cambridge (1995).
  105.16 -*)
  105.17 -
  105.18 -use_thys ["ECR"];
   106.1 --- a/src/ZF/Constructible/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
   106.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
   106.3 @@ -1,8 +0,0 @@
   106.4 -(*  Title:      ZF/Constructible/ROOT.ML
   106.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   106.6 -    Copyright   2002  University of Cambridge
   106.7 -
   106.8 -Inner Models, Absoluteness and Consistency Proofs.
   106.9 -*)
  106.10 -
  106.11 -use_thys ["DPow_absolute", "AC_in_L", "Rank_Separation"];
   107.1 --- a/src/ZF/IMP/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
   107.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
   107.3 @@ -1,14 +0,0 @@
   107.4 -(*  Title:      ZF/IMP/ROOT.ML
   107.5 -    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
   107.6 -    Copyright   1994 TUM
   107.7 -
   107.8 -Executes the formalization of the denotational and operational semantics of a
   107.9 -simple while-language, including an equivalence proof. The whole development
  107.10 -essentially formalizes/transcribes chapters 2 and 5 of
  107.11 -
  107.12 -Glynn Winskel. The Formal Semantics of Programming Languages.
  107.13 -MIT Press, 1993.
  107.14 -
  107.15 -*)
  107.16 -
  107.17 -use_thys ["Equiv"];
   108.1 --- a/src/ZF/Induct/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
   108.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
   108.3 @@ -1,30 +0,0 @@
   108.4 -(*  Title:      ZF/Induct/ROOT.ML
   108.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   108.6 -    Copyright   2001  University of Cambridge
   108.7 -
   108.8 -Inductive definitions.
   108.9 -*)
  108.10 -
  108.11 -use_thys [
  108.12 -(** Datatypes **)
  108.13 -  "Datatypes",       (*sample datatypes*)
  108.14 -  "Binary_Trees",    (*binary trees*)
  108.15 -  "Term",            (*recursion over the list functor*)
  108.16 -  "Ntree",           (*variable-branching trees; function demo*)
  108.17 -  "Tree_Forest",     (*mutual recursion*)
  108.18 -  "Brouwer",         (*Infinite-branching trees*)
  108.19 -  "Mutil",           (*mutilated chess board*)
  108.20 -
  108.21 -(*by Sidi Ehmety: Multisets.  A parent is FoldSet, the "fold" function for
  108.22 -finite sets*)
  108.23 -  "Multiset",
  108.24 -  "Rmap",            (*mapping a relation over a list*)
  108.25 -  "PropLog",         (*completeness of propositional logic*)
  108.26 -
  108.27 -(*two Coq examples by Christine Paulin-Mohring*)
  108.28 -  "ListN",
  108.29 -  "Acc",
  108.30 -
  108.31 -  "Comb",            (*Combinatory Logic example*)
  108.32 -  "Primrec"          (*Primitive recursive functions*)
  108.33 -];
   109.1 --- a/src/ZF/IsaMakefile	Tue Aug 07 23:38:18 2012 +0200
   109.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
   109.3 @@ -1,149 +0,0 @@
   109.4 -#
   109.5 -# IsaMakefile for ZF
   109.6 -#
   109.7 -
   109.8 -## targets
   109.9 -
  109.10 -default: ZF
  109.11 -images: ZF
  109.12 -
  109.13 -#Note: keep targets sorted
  109.14 -test: ZF-AC ZF-Coind ZF-Constructible ZF-IMP ZF-Induct ZF-Resid ZF-UNITY ZF-ex
  109.15 -all: images test
  109.16 -full: all
  109.17 -smlnj: all
  109.18 -
  109.19 -
  109.20 -## global settings
  109.21 -
  109.22 -SRC = $(ISABELLE_HOME)/src
  109.23 -OUT = $(ISABELLE_OUTPUT)
  109.24 -LOG = $(OUT)/log
  109.25 -
  109.26 -
  109.27 -## ZF
  109.28 -
  109.29 -ZF: FOL $(OUT)/ZF
  109.30 -
  109.31 -FOL:
  109.32 -	@cd $(SRC)/FOL; $(ISABELLE_TOOL) make FOL
  109.33 -
  109.34 -$(OUT)/ZF: $(OUT)/FOL AC.thy Arith.thy ArithSimp.thy Bin.thy Bool.thy	\
  109.35 -  Cardinal.thy CardinalArith.thy Cardinal_AC.thy Datatype_ZF.thy	\
  109.36 -  Epsilon.thy EquivClass.thy Finite.thy Fixedpt.thy Inductive_ZF.thy	\
  109.37 -  InfDatatype.thy Int_ZF.thy IntArith.thy IntDiv_ZF.thy List_ZF.thy	\
  109.38 -  Main.thy Main_ZF.thy Main_ZFC.thy Nat_ZF.thy OrdQuant.thy Order.thy	\
  109.39 -  OrderArith.thy OrderType.thy Ordinal.thy Perm.thy QPair.thy		\
  109.40 -  QUniv.thy ROOT.ML Sum.thy Tools/cartprod.ML				\
  109.41 -  Tools/datatype_package.ML Tools/ind_cases.ML Tools/induct_tacs.ML	\
  109.42 -  Tools/inductive_package.ML Tools/numeral_syntax.ML			\
  109.43 -  Tools/primrec_package.ML Tools/typechk.ML Trancl.thy Univ.thy WF.thy	\
  109.44 -  ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy ind_syntax.ML	\
  109.45 -  int_arith.ML pair.thy simpdata.ML upair.thy
  109.46 -	@$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/FOL ZF
  109.47 -
  109.48 -
  109.49 -## ZF-AC
  109.50 -
  109.51 -ZF-AC: ZF $(LOG)/ZF-AC.gz
  109.52 -
  109.53 -$(LOG)/ZF-AC.gz: $(OUT)/ZF AC/ROOT.ML AC/AC15_WO6.thy AC/AC16_WO4.thy	\
  109.54 -  AC/AC16_lemmas.thy AC/AC17_AC1.thy AC/AC18_AC19.thy AC/AC7_AC9.thy	\
  109.55 -  AC/AC_Equiv.thy AC/Cardinal_aux.thy AC/DC.thy AC/HH.thy		\
  109.56 -  AC/Hartog.thy AC/WO1_AC.thy AC/WO1_WO7.thy AC/WO2_AC16.thy		\
  109.57 -  AC/WO6_WO1.thy AC/document/root.bib AC/document/root.tex
  109.58 -	@$(ISABELLE_TOOL) usedir -g true $(OUT)/ZF AC
  109.59 -
  109.60 -
  109.61 -## ZF-Coind
  109.62 -
  109.63 -ZF-Coind: ZF $(LOG)/ZF-Coind.gz
  109.64 -
  109.65 -$(LOG)/ZF-Coind.gz: $(OUT)/ZF Coind/Dynamic.thy Coind/ECR.thy		\
  109.66 -  Coind/Language.thy Coind/Map.thy Coind/ROOT.ML Coind/Static.thy	\
  109.67 -  Coind/Types.thy Coind/Values.thy
  109.68 -	@$(ISABELLE_TOOL) usedir $(OUT)/ZF Coind
  109.69 -
  109.70 -
  109.71 -## ZF-Constructible
  109.72 -
  109.73 -ZF-Constructible: ZF $(LOG)/ZF-Constructible.gz
  109.74 -
  109.75 -$(LOG)/ZF-Constructible.gz: $(OUT)/ZF Constructible/ROOT.ML		\
  109.76 -  Constructible/Datatype_absolute.thy Constructible/DPow_absolute.thy	\
  109.77 -  Constructible/Formula.thy Constructible/Internalize.thy		\
  109.78 -  Constructible/AC_in_L.thy Constructible/Relative.thy			\
  109.79 -  Constructible/L_axioms.thy Constructible/Wellorderings.thy		\
  109.80 -  Constructible/MetaExists.thy Constructible/Normal.thy			\
  109.81 -  Constructible/Rank.thy Constructible/Rank_Separation.thy		\
  109.82 -  Constructible/Rec_Separation.thy Constructible/Separation.thy		\
  109.83 -  Constructible/Satisfies_absolute.thy Constructible/WF_absolute.thy	\
  109.84 -  Constructible/Reflection.thy Constructible/WFrec.thy			\
  109.85 -  Constructible/document/root.bib Constructible/document/root.tex
  109.86 -	@$(ISABELLE_TOOL) usedir -g true $(OUT)/ZF Constructible
  109.87 -
  109.88 -
  109.89 -## ZF-IMP
  109.90 -
  109.91 -ZF-IMP: ZF $(LOG)/ZF-IMP.gz
  109.92 -
  109.93 -$(LOG)/ZF-IMP.gz: $(OUT)/ZF IMP/Com.thy IMP/Denotation.thy	\
  109.94 -  IMP/Equiv.thy IMP/ROOT.ML IMP/document/root.bib		\
  109.95 -  IMP/document/root.tex
  109.96 -	@$(ISABELLE_TOOL) usedir $(OUT)/ZF IMP
  109.97 -
  109.98 -
  109.99 -## ZF-Resid
 109.100 -
 109.101 -ZF-Resid: ZF $(LOG)/ZF-Resid.gz
 109.102 -
 109.103 -$(LOG)/ZF-Resid.gz: $(OUT)/ZF Resid/ROOT.ML Resid/Confluence.thy	\
 109.104 -  Resid/Redex.thy Resid/Reduction.thy Resid/Residuals.thy		\
 109.105 -  Resid/Substitution.thy
 109.106 -	@$(ISABELLE_TOOL) usedir $(OUT)/ZF Resid
 109.107 -
 109.108 -
 109.109 -## ZF-UNITY
 109.110 -
 109.111 -ZF-UNITY: ZF $(LOG)/ZF-UNITY.gz
 109.112 -
 109.113 -$(LOG)/ZF-UNITY.gz: $(OUT)/ZF UNITY/ROOT.ML UNITY/Comp.thy		\
 109.114 -  UNITY/Constrains.thy UNITY/FP.thy UNITY/GenPrefix.thy UNITY/Guar.thy	\
 109.115 -  UNITY/Mutex.thy UNITY/State.thy UNITY/SubstAx.thy UNITY/UNITY.thy	\
 109.116 -  UNITY/Union.thy UNITY/AllocBase.thy UNITY/AllocImpl.thy		\
 109.117 -  UNITY/ClientImpl.thy UNITY/Distributor.thy UNITY/Follows.thy		\
 109.118 -  UNITY/Increasing.thy UNITY/Merge.thy UNITY/Monotonicity.thy		\
 109.119 -  UNITY/MultisetSum.thy UNITY/WFair.thy
 109.120 -	@$(ISABELLE_TOOL) usedir $(OUT)/ZF UNITY
 109.121 -
 109.122 -
 109.123 -## ZF-Induct
 109.124 -
 109.125 -ZF-Induct: ZF $(LOG)/ZF-Induct.gz
 109.126 -
 109.127 -$(LOG)/ZF-Induct.gz: $(OUT)/ZF Induct/ROOT.ML Induct/Acc.thy		\
 109.128 -  Induct/Binary_Trees.thy Induct/Brouwer.thy Induct/Comb.thy		\
 109.129 -  Induct/Datatypes.thy Induct/FoldSet.thy Induct/ListN.thy		\
 109.130 -  Induct/Multiset.thy Induct/Mutil.thy Induct/Ntree.thy			\
 109.131 -  Induct/Primrec.thy Induct/PropLog.thy Induct/Rmap.thy			\
 109.132 -  Induct/Term.thy Induct/Tree_Forest.thy Induct/document/root.tex
 109.133 -	@$(ISABELLE_TOOL) usedir $(OUT)/ZF Induct
 109.134 -
 109.135 -
 109.136 -## ZF-ex
 109.137 -
 109.138 -ZF-ex: ZF $(LOG)/ZF-ex.gz
 109.139 -
 109.140 -$(LOG)/ZF-ex.gz: $(OUT)/ZF ex/ROOT.ML ex/BinEx.thy ex/CoUnit.thy	\
 109.141 -  ex/Commutation.thy ex/Group.thy ex/Limit.thy ex/LList.thy		\
 109.142 -  ex/Primes.thy ex/NatSum.thy ex/Ramsey.thy ex/Ring.thy ex/misc.thy
 109.143 -	@$(ISABELLE_TOOL) usedir $(OUT)/ZF ex
 109.144 -
 109.145 -
 109.146 -## clean
 109.147 -
 109.148 -clean:
 109.149 -	@rm -f $(OUT)/ZF $(LOG)/ZF.gz $(LOG)/ZF-AC.gz		\
 109.150 -	  $(LOG)/ZF-Coind.gz $(LOG)/ZF-Constructible.gz		\
 109.151 -	  $(LOG)/ZF-ex.gz $(LOG)/ZF-IMP.gz $(LOG)/ZF-Induct.gz	\
 109.152 -	  $(LOG)/ZF-Resid.gz $(LOG)/ZF-UNITY.gz
   110.1 --- a/src/ZF/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
   110.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
   110.3 @@ -1,11 +0,0 @@
   110.4 -(*  Title:      ZF/ROOT.ML
   110.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   110.6 -    Copyright   1993  University of Cambridge
   110.7 -
   110.8 -Zermelo-Fraenkel Set Theory on top of classical First-Order Logic.
   110.9 -This theory is the work of Martin Coen, Philippe Noel and Lawrence
  110.10 -Paulson.
  110.11 -*)
  110.12 -
  110.13 -use_thys ["Main", "Main_ZFC"];
  110.14 -
   111.1 --- a/src/ZF/Resid/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
   111.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
   111.3 @@ -1,14 +0,0 @@
   111.4 -(*  Title:      ZF/Resid/ROOT.ML
   111.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   111.6 -    Copyright   1995  University of Cambridge
   111.7 -
   111.8 -Executes the Residuals example.
   111.9 -This is a proof of the Church-Rosser Theorem for the untyped lambda-calculus.
  111.10 -
  111.11 -By Ole Rasmussen, following the Coq proof given in
  111.12 -
  111.13 -Gerard Huet.  Residual Theory in Lambda-Calculus: A Formal Development.
  111.14 -J. Functional Programming 4(3) 1994, 371-394.
  111.15 -*)
  111.16 -
  111.17 -use_thys ["Confluence"];
   112.1 --- a/src/ZF/UNITY/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
   112.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
   112.3 @@ -1,17 +0,0 @@
   112.4 -(*  Title:      ZF/UNITY/ROOT.ML
   112.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   112.6 -    Copyright   1998  University of Cambridge
   112.7 -
   112.8 -ZF/UNITY proofs.
   112.9 -*)
  112.10 -
  112.11 -use_thys [
  112.12 -  (*Simple examples: no composition*)
  112.13 -  "Mutex",
  112.14 -
  112.15 -  (*Basic meta-theory*)
  112.16 -  "Guar",
  112.17 -
  112.18 -  (*Prefix relation; the Allocator example*)
  112.19 -  "Distributor", "Merge", "ClientImpl", "AllocImpl"
  112.20 -];
   113.1 --- a/src/ZF/ex/ROOT.ML	Tue Aug 07 23:38:18 2012 +0200
   113.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
   113.3 @@ -1,18 +0,0 @@
   113.4 -(*  Title:      ZF/ex/ROOT.ML
   113.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   113.6 -    Copyright   1993  University of Cambridge
   113.7 -
   113.8 -Miscellaneous examples for Zermelo-Fraenkel Set Theory.
   113.9 -*)
  113.10 -
  113.11 -use_thys [
  113.12 -  "misc",
  113.13 -  "Ring",             (*abstract algebra*)
  113.14 -  "Commutation",      (*abstract Church-Rosser theory*)
  113.15 -  "Primes",           (*GCD theory*)
  113.16 -  "NatSum",           (*Summing integers, squares, cubes, etc.*)
  113.17 -  "Ramsey",           (*Simple form of Ramsey's theorem*)
  113.18 -  "Limit",            (*Inverse limit construction of domains*)
  113.19 -  "BinEx",            (*Binary integer arithmetic*)
  113.20 -  "LList", "CoUnit"   (*CoDatatypes*)
  113.21 -];