# HG changeset patch # User wenzelm # Date 1344375785 -7200 # Node ID a5e3ba7cbb2a667ceb4f659bf9749e33c9b44f4d # Parent 866f6d5baf4c123743327419e4c95803f476c050 discontinued obsolete IsaMakefile and ROOT.ML files from the Isabelle distribution; diff -r 866f6d5baf4c -r a5e3ba7cbb2a NEWS --- a/NEWS Tue Aug 07 23:38:18 2012 +0200 +++ b/NEWS Tue Aug 07 23:43:05 2012 +0200 @@ -80,6 +80,12 @@ build" tool and its examples. Eventual INCOMPATIBILITY, as isabelle usedir / make / makeall are rendered obsolete. +* Discontinued obsolete IsaMakefile and ROOT.ML files from the +Isabelle distribution, except for rudimentary src/HOL/IsaMakefile that +provides some traditional targets that invoke "isabelle build". Note +that this is inefficient! Applications of Isabelle/HOL involving +"isabelle make" should be upgraded to use "isabelle build" directly. + * Discontinued obsolete Isabelle/build script, it is superseded by the regular isabelle build tool. For example: diff -r 866f6d5baf4c -r a5e3ba7cbb2a doc-src/System/Thy/Misc.thy --- a/doc-src/System/Thy/Misc.thy Tue Aug 07 23:38:18 2012 +0200 +++ b/doc-src/System/Thy/Misc.thy Tue Aug 07 23:43:05 2012 +0200 @@ -222,15 +222,6 @@ *} -subsubsection {* Examples *} - -text {* - Refer to the @{verbatim IsaMakefile}s of the Isabelle distribution's - object-logics as a model for your own developments. For example, - see @{file "~~/src/FOL/IsaMakefile"}. -*} - - section {* Make all logics *} text {* The @{tool_def makeall} tool applies Isabelle make to any diff -r 866f6d5baf4c -r a5e3ba7cbb2a doc-src/System/Thy/Presentation.thy --- a/doc-src/System/Thy/Presentation.thy Tue Aug 07 23:38:18 2012 +0200 +++ b/doc-src/System/Thy/Presentation.thy Tue Aug 07 23:43:05 2012 +0200 @@ -242,7 +242,7 @@ meant to cover all of the sub-session directories at the same time (this is the deeper reasong why @{verbatim IsaMakefile} is not made part of the initial session directory created by @{tool mkdir}). - See @{file "~~/src/HOL/IsaMakefile"} for a full-blown example. *} +*} section {* Running Isabelle sessions \label{sec:tool-usedir} *} @@ -419,15 +419,6 @@ *} -subsubsection {* Examples *} - -text {* Refer to the @{verbatim IsaMakefile}s of the Isabelle - distribution's object-logics as a model for your own developments. - For example, see @{file "~~/src/FOL/IsaMakefile"}. The @{tool_ref - mkdir} tool creates @{verbatim IsaMakefile}s with proper invocation - of @{tool usedir} as well. *} - - section {* Preparing Isabelle session documents \label{sec:tool-document} *} diff -r 866f6d5baf4c -r a5e3ba7cbb2a doc-src/System/Thy/document/Misc.tex --- a/doc-src/System/Thy/document/Misc.tex Tue Aug 07 23:38:18 2012 +0200 +++ b/doc-src/System/Thy/document/Misc.tex Tue Aug 07 23:43:05 2012 +0200 @@ -262,17 +262,6 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsubsection{Examples% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Refer to the \verb|IsaMakefile|s of the Isabelle distribution's - object-logics as a model for your own developments. For example, - see \verb|~~/src/FOL/IsaMakefile|.% -\end{isamarkuptext}% -\isamarkuptrue% -% \isamarkupsection{Make all logics% } \isamarkuptrue% diff -r 866f6d5baf4c -r a5e3ba7cbb2a doc-src/System/Thy/document/Presentation.tex --- a/doc-src/System/Thy/document/Presentation.tex Tue Aug 07 23:38:18 2012 +0200 +++ b/doc-src/System/Thy/document/Presentation.tex Tue Aug 07 23:43:05 2012 +0200 @@ -257,8 +257,7 @@ manual editing of the generated \verb|IsaMakefile|, which is meant to cover all of the sub-session directories at the same time (this is the deeper reasong why \verb|IsaMakefile| is not made - part of the initial session directory created by \hyperlink{tool.mkdir}{\mbox{\isa{\isatool{mkdir}}}}). - See \verb|~~/src/HOL/IsaMakefile| for a full-blown example.% + part of the initial session directory created by \hyperlink{tool.mkdir}{\mbox{\isa{\isatool{mkdir}}}}).% \end{isamarkuptext}% \isamarkuptrue% % @@ -430,18 +429,6 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsubsection{Examples% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Refer to the \verb|IsaMakefile|s of the Isabelle - distribution's object-logics as a model for your own developments. - 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 - of \hyperlink{tool.usedir}{\mbox{\isa{\isatool{usedir}}}} as well.% -\end{isamarkuptext}% -\isamarkuptrue% -% \isamarkupsection{Preparing Isabelle session documents \label{sec:tool-document}% } diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/CCL/IsaMakefile --- a/src/CCL/IsaMakefile Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,48 +0,0 @@ -# -# IsaMakefile for CCL -# - -## targets - -default: CCL -images: CCL -test: CCL-ex -all: images test -full: all -smlnj: all - - -## global settings - -SRC = $(ISABELLE_HOME)/src -OUT = $(ISABELLE_OUTPUT) -LOG = $(OUT)/log - - -## CCL - -CCL: FOL $(OUT)/CCL - -FOL: - @cd $(SRC)/FOL; $(ISABELLE_TOOL) make FOL - -$(OUT)/FOL: FOL - -$(OUT)/CCL: $(OUT)/FOL CCL.thy Fix.thy Gfp.thy Hered.thy Lfp.thy ROOT.ML \ - Set.thy Term.thy Trancl.thy Type.thy Wfd.thy - @$(ISABELLE_TOOL) usedir -b -r $(OUT)/FOL CCL - - -## CCL-ex - -CCL-ex: CCL $(LOG)/CCL-ex.gz - -$(LOG)/CCL-ex.gz: $(OUT)/CCL ex/Flag.thy ex/List.thy ex/Nat.thy ex/ROOT.ML \ - ex/Stream.thy - @$(ISABELLE_TOOL) usedir $(OUT)/CCL ex - - -## clean - -clean: - @rm -f $(OUT)/CCL $(LOG)/CCL.gz $(LOG)/CCL-ex.gz diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/CCL/ROOT.ML --- a/src/CCL/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,11 +0,0 @@ -(* Title: CCL/ROOT.ML - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -Classical Computational Logic based on First-Order Logic. - -A computational logic for an untyped functional language with -evaluation to weak head-normal form. -*) - -use_thys ["Wfd", "Fix"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/CCL/ex/ROOT.ML --- a/src/CCL/ex/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -(* Title: CCL/ex/ROOT.ML - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -Examples for Classical Computational Logic. -*) - -use_thys ["Nat", "List", "Stream", "Flag"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/CTT/IsaMakefile --- a/src/CTT/IsaMakefile Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,46 +0,0 @@ -# -# IsaMakefile for CTT -# - -## targets - -default: CTT -images: CTT -test: CTT-ex -all: images test -full: all -smlnj: all - - -## global settings - -SRC = $(ISABELLE_HOME)/src -OUT = $(ISABELLE_OUTPUT) -LOG = $(OUT)/log - - -## CTT - -CTT: Pure $(OUT)/CTT - -Pure: - @cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure - -$(OUT)/CTT: $(OUT)/Pure $(SRC)/Provers/typedsimp.ML Arith.thy \ - Bool.thy CTT.thy Main.thy ROOT.ML rew.ML - @$(ISABELLE_TOOL) usedir -b $(OUT)/Pure CTT - - -## CTT-ex - -CTT-ex: CTT $(LOG)/CTT-ex.gz - -$(LOG)/CTT-ex.gz: $(OUT)/CTT ex/ROOT.ML ex/Elimination.thy \ - ex/Equality.thy ex/Synthesis.thy ex/Typechecking.thy - @$(ISABELLE_TOOL) usedir $(OUT)/CTT ex - - -## clean - -clean: - @rm -f $(OUT)/CTT $(LOG)/CTT.gz $(LOG)/CTT-ex.gz diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/CTT/ROOT.ML --- a/src/CTT/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ -(* Title: CTT/ROOT.ML - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1991 University of Cambridge -*) - -use_thys ["Main"]; - diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/CTT/ex/ROOT.ML --- a/src/CTT/ex/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -(* Title: CTT/ex/ROOT.ML - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1991 University of Cambridge - -Examples for Constructive Type Theory. -*) - -use_thys ["Typechecking", "Elimination", "Equality", "Synthesis"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/Cube/IsaMakefile --- a/src/Cube/IsaMakefile Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,36 +0,0 @@ -# -# IsaMakefile for Cube -# - -## targets - -default: Pure-Cube -images: -test: Pure-Cube -all: images test -full: all -smlnj: all - - -## global settings - -SRC = $(ISABELLE_HOME)/src -OUT = $(ISABELLE_OUTPUT) -LOG = $(OUT)/log - - -## Pure-Cube - -Pure-Cube: Pure $(LOG)/Pure-Cube.gz - -Pure: - @cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure - -$(LOG)/Pure-Cube.gz: $(OUT)/Pure Cube.thy Example.thy ROOT.ML - @cd ..; $(ISABELLE_TOOL) usedir $(OUT)/Pure Cube - - -## clean - -clean: - @rm -f $(LOG)/Pure-Cube.gz diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/Cube/ROOT.ML --- a/src/Cube/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -(* Title: Cube/ROOT.ML - Author: Tobias Nipkow - Copyright 1992 University of Cambridge - -The Lambda-Cube a la Barendregt. -*) - -use_thys ["Example"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/FOL/IsaMakefile --- a/src/FOL/IsaMakefile Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,63 +0,0 @@ -# -# IsaMakefile for FOL -# - -## targets - -default: FOL -images: FOL -test: FOL-ex -all: images test -full: all -smlnj: all - - -## global settings - -SRC = $(ISABELLE_HOME)/src -OUT = $(ISABELLE_OUTPUT) -LOG = $(OUT)/log - - -## FOL - -FOL: Pure $(OUT)/FOL - -Pure: - @cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure - -$(OUT)/Pure: Pure - -$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML \ - $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ - $(SRC)/Tools/case_product.ML $(SRC)/Tools/misc_legacy.ML \ - $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/IsaPlanner/isand.ML \ - $(SRC)/Tools/IsaPlanner/rw_tools.ML \ - $(SRC)/Tools/IsaPlanner/rw_inst.ML $(SRC)/Tools/eqsubst.ML \ - $(SRC)/Provers/hypsubst.ML $(SRC)/Tools/induct.ML \ - $(SRC)/Tools/intuitionistic.ML $(SRC)/Tools/atomize_elim.ML \ - $(SRC)/Tools/project_rule.ML $(SRC)/Provers/quantifier1.ML \ - $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML \ - document/root.tex fologic.ML intprover.ML simpdata.ML - @$(ISABELLE_TOOL) usedir -p 2 -b $(OUT)/Pure FOL - - -## FOL-ex - -FOL-ex: FOL $(LOG)/FOL-ex.gz - -$(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy ex/If.thy \ - ex/Nat.thy ex/Nat_Class.thy ex/Natural_Numbers.thy \ - ex/Locale_Test/Locale_Test.thy ex/Locale_Test/Locale_Test1.thy \ - ex/Locale_Test/Locale_Test2.thy ex/Locale_Test/Locale_Test3.thy \ - ex/Miniscope.thy ex/Prolog.thy ex/ROOT.ML ex/Classical.thy \ - ex/document/root.tex ex/Foundation.thy ex/Intuitionistic.thy \ - ex/Intro.thy ex/Propositional_Int.thy ex/Propositional_Cla.thy \ - ex/Quantifiers_Int.thy ex/Quantifiers_Cla.thy - @$(ISABELLE_TOOL) usedir $(OUT)/FOL ex - - -## clean - -clean: - @rm -f $(OUT)/FOL $(LOG)/FOL.gz $(LOG)/FOL-ex.gz diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/FOL/ROOT.ML --- a/src/FOL/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -(* First-Order Logic with Natural Deduction *) - -use_thys ["FOL"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/FOL/ex/ROOT.ML --- a/src/FOL/ex/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,19 +0,0 @@ -use_thys [ - "First_Order_Logic", - "Natural_Numbers", - "Intro", - "Nat", - "Nat_Class", - "Foundation", - "Prolog", - "Intuitionistic", - "Propositional_Int", - "Quantifiers_Int", - "Classical", - "Propositional_Cla", - "Quantifiers_Cla", - "Miniscope", - "If" -]; - -no_document use_thy "Locale_Test/Locale_Test"; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/FOLP/IsaMakefile --- a/src/FOLP/IsaMakefile Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,48 +0,0 @@ -# -# IsaMakefile for FOLP -# - -## targets - -default: FOLP -images: FOLP -test: FOLP-ex -all: images test -full: all -smlnj: all - - -## global settings - -SRC = $(ISABELLE_HOME)/src -OUT = $(ISABELLE_OUTPUT) -LOG = $(OUT)/log - - -## FOLP - -FOLP: Pure $(OUT)/FOLP - -Pure: - @cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure - -$(OUT)/FOLP: $(OUT)/Pure FOLP.thy IFOLP.thy ROOT.ML classical.ML \ - hypsubst.ML intprover.ML simp.ML simpdata.ML $(SRC)/Tools/misc_legacy.ML - @$(ISABELLE_TOOL) usedir -b $(OUT)/Pure FOLP - - -## FOLP-ex - -FOLP-ex: FOLP $(LOG)/FOLP-ex.gz - -$(LOG)/FOLP-ex.gz: $(OUT)/FOLP ex/ROOT.ML ex/Foundation.thy ex/If.thy \ - ex/Intro.thy ex/Nat.thy ex/Intuitionistic.thy ex/Classical.thy \ - ex/Propositional_Int.thy ex/Propositional_Cla.thy \ - ex/Quantifiers_Int.thy ex/Quantifiers_Cla.thy - @$(ISABELLE_TOOL) usedir $(OUT)/FOLP ex - - -## clean - -clean: - @rm -f $(OUT)/FOLP $(LOG)/FOLP.gz $(LOG)/FOLP-ex.gz diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/FOLP/ROOT.ML --- a/src/FOLP/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,11 +0,0 @@ -(* Title: FOLP/ROOT.ML - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -Modifed version of Lawrence Paulson's FOL that contains proof terms. - -Presence of unknown proof term means that matching does not behave as expected. -*) - -use_thys ["FOLP"]; - diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/FOLP/ex/ROOT.ML --- a/src/FOLP/ex/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,19 +0,0 @@ -(* Title: FOLP/ex/ROOT.ML - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1992 University of Cambridge - -Examples for First-Order Logic. -*) - -use_thys [ - "Intro", - "Nat", - "Foundation", - "If", - "Intuitionistic", - "Classical", - "Propositional_Int", - "Quantifiers_Int", - "Propositional_Cla", - "Quantifiers_Cla" -]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Algebra/ROOT.ML --- a/src/HOL/Algebra/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,35 +0,0 @@ -(* Author: Clemens Ballarin, started 24 September 1999 - -The Isabelle Algebraic Library. -*) - -(* Preliminaries from set and number theory *) -no_document use_thys [ - "~~/src/HOL/Library/FuncSet", - "~~/src/HOL/Old_Number_Theory/Primes", - "~~/src/HOL/Library/Binomial", - "~~/src/HOL/Library/Permutation" -]; - - -(*** New development, based on explicit structures ***) - -use_thys [ - (* Groups *) - "FiniteProduct", (* Product operator for commutative groups *) - "Sylow", (* Sylow's theorem *) - "Bij", (* Automorphism Groups *) - - (* Rings *) - "Divisibility", (* Rings *) - "IntRing", (* Ideals and residue classes *) - "UnivPoly" (* Polynomials *) -]; - - -(*** Old development, based on axiomatic type classes ***) - -no_document use_thys [ - "abstract/Abstract", (*The ring theory*) - "poly/Polynomial" (*The full theory*) -]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Auth/ROOT.ML --- a/src/HOL/Auth/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ -use_thys [ - "Auth_Shared", - "Auth_Public", - "Smartcard/Auth_Smartcard", - "Guard/Auth_Guard_Shared", - "Guard/Auth_Guard_Public" -]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Bali/ROOT.ML --- a/src/HOL/Bali/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -use_thys ["AxExample", "AxSound", "AxCompl", "Trans"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Boogie/Examples/ROOT.ML --- a/src/HOL/Boogie/Examples/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -use_thys ["Boogie_Max_Stepwise", "Boogie_Max", "Boogie_Dijkstra", "VCC_Max"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Boogie/ROOT.ML --- a/src/HOL/Boogie/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -use_thys ["Boogie"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Codegenerator_Test/ROOT.ML --- a/src/HOL/Codegenerator_Test/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -use_thys ["Generate", "Generate_Pretty", "RBT_Set_Test"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Datatype_Benchmark/ROOT.ML --- a/src/HOL/Datatype_Benchmark/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -(* Title: HOL/Datatype_Benchmark/ROOT.ML - -Some rather large datatype examples (from John Harrison). -*) - -Toplevel.timing := true; - -use_thys ["Brackin", "Instructions", "SML", "Verilog"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Decision_Procs/ROOT.ML --- a/src/HOL/Decision_Procs/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -use_thys ["Decision_Procs"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/HOLCF/FOCUS/ROOT.ML --- a/src/HOL/HOLCF/FOCUS/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -use_thys ["Fstreams", "FOCUS", "Buffer_adm"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/HOLCF/IMP/ROOT.ML --- a/src/HOL/HOLCF/IMP/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -use_thys ["HoareEx"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/HOLCF/IOA/ABP/ROOT.ML --- a/src/HOL/HOLCF/IOA/ABP/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -(* Title: HOL/HOLCF/IOA/ABP/ROOT.ML - Author: Olaf Mueller - -This is the ROOT file for the Alternating Bit Protocol performed in -I/O-Automata. -*) - -use_thys ["Correctness"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/HOLCF/IOA/NTP/ROOT.ML --- a/src/HOL/HOLCF/IOA/NTP/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -(* Title: HOL/HOLCF/IOA/NTP/ROOT.ML - Author: Tobias Nipkow & Konrad Slind - -This is the ROOT file for a network transmission protocol (NTP -subdirectory), performed in the I/O automata formalization by Olaf -Mueller. -*) - -use_thys ["Correctness"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/HOLCF/IOA/ROOT.ML --- a/src/HOL/HOLCF/IOA/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -(* Title: HOL/HOLCF/IOA/ROOT.ML - Author: Olaf Mueller - -Formalization of a semantic model of I/O-Automata. See README.html -for details. -*) - -use_thys ["meta_theory/Abstraction"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/HOLCF/IOA/Storage/ROOT.ML --- a/src/HOL/HOLCF/IOA/Storage/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,6 +0,0 @@ -(* Title: HOL/HOLCF/IOA/Storage/ROOT.ML - Author: Olaf Mueller - -Memory storage case study. -*) -use_thys ["Correctness"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/HOLCF/IOA/ex/ROOT.ML --- a/src/HOL/HOLCF/IOA/ex/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,5 +0,0 @@ -(* Title: HOL/HOLCF/IOA/ex/ROOT.ML - Author: Olaf Mueller -*) - -use_thys ["TrivEx", "TrivEx2"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/HOLCF/IsaMakefile --- a/src/HOL/HOLCF/IsaMakefile Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,234 +0,0 @@ -# -# IsaMakefile for HOLCF -# - -## targets - -default: HOLCF -images: HOLCF IOA -test: \ - HOLCF-FOCUS \ - HOLCF-IMP \ - HOLCF-Library \ - HOLCF-Tutorial \ - HOLCF-ex \ - IOA-ABP \ - IOA-NTP \ - IOA-Storage \ - IOA-ex -all: images test -full: all - - -## global settings - -SRC = $(ISABELLE_HOME)/src -OUT = $(ISABELLE_OUTPUT) -LOG = $(OUT)/log - - -## HOLCF - -HOLCF: HOL $(OUT)/HOLCF - -HOL: - @cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL - -$(OUT)/HOLCF: $(OUT)/HOL \ - ROOT.ML \ - Adm.thy \ - Algebraic.thy \ - Bifinite.thy \ - Cfun.thy \ - Compact_Basis.thy \ - Completion.thy \ - Cont.thy \ - ConvexPD.thy \ - Cpodef.thy \ - Cprod.thy \ - Discrete.thy \ - Deflation.thy \ - Domain.thy \ - Domain_Aux.thy \ - Fixrec.thy \ - Fix.thy \ - Fun_Cpo.thy \ - HOLCF.thy \ - Lift.thy \ - LowerPD.thy \ - Map_Functions.thy \ - One.thy \ - Pcpo.thy \ - Plain_HOLCF.thy \ - Porder.thy \ - Powerdomains.thy \ - Product_Cpo.thy \ - Representable.thy \ - Sfun.thy \ - Sprod.thy \ - Ssum.thy \ - Tr.thy \ - Universal.thy \ - UpperPD.thy \ - Up.thy \ - Tools/cont_consts.ML \ - Tools/cont_proc.ML \ - Tools/holcf_library.ML \ - Tools/Domain/domain.ML \ - Tools/Domain/domain_axioms.ML \ - Tools/Domain/domain_constructors.ML \ - Tools/Domain/domain_induction.ML \ - Tools/Domain/domain_isomorphism.ML \ - Tools/Domain/domain_take_proofs.ML \ - Tools/cpodef.ML \ - Tools/domaindef.ML \ - Tools/fixrec.ML \ - document/root.tex - @$(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOLCF - - -## HOLCF-Tutorial - -HOLCF-Tutorial: HOLCF $(LOG)/HOLCF-Tutorial.gz - -$(LOG)/HOLCF-Tutorial.gz: $(OUT)/HOLCF \ - Tutorial/Domain_ex.thy \ - Tutorial/Fixrec_ex.thy \ - Tutorial/New_Domain.thy \ - Tutorial/document/root.tex \ - Tutorial/ROOT.ML - @$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Tutorial - - -## HOLCF-Library - -HOLCF-Library: HOLCF $(LOG)/HOLCF-Library.gz - -$(LOG)/HOLCF-Library.gz: $(OUT)/HOLCF \ - Library/Defl_Bifinite.thy \ - Library/Bool_Discrete.thy \ - Library/Char_Discrete.thy \ - Library/HOL_Cpo.thy \ - Library/Int_Discrete.thy \ - Library/List_Cpo.thy \ - Library/List_Predomain.thy \ - Library/Nat_Discrete.thy \ - Library/Option_Cpo.thy \ - Library/Stream.thy \ - Library/Sum_Cpo.thy \ - Library/HOLCF_Library.thy \ - Library/ROOT.ML - @$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Library - - -## HOLCF-IMP - -HOLCF-IMP: HOLCF $(LOG)/HOLCF-IMP.gz - -$(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF IMP/HoareEx.thy \ - IMP/Denotational.thy IMP/ROOT.ML IMP/document/root.tex - @$(ISABELLE_TOOL) usedir $(OUT)/HOLCF IMP - - -## HOLCF-ex - -HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz - -$(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF \ - ../Library/Extended_Nat.thy \ - ex/Concurrency_Monad.thy \ - ex/Dagstuhl.thy \ - ex/Dnat.thy \ - ex/Domain_Proofs.thy \ - ex/Fix2.thy \ - ex/Focus_ex.thy \ - ex/Hoare.thy \ - ex/Letrec.thy \ - ex/Loop.thy \ - ex/Pattern_Match.thy \ - ex/Powerdomain_ex.thy \ - ex/ROOT.ML - @$(ISABELLE_TOOL) usedir $(OUT)/HOLCF ex - - -## HOLCF-FOCUS - -HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz - -$(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF \ - Library/Stream.thy \ - FOCUS/Fstreams.thy \ - FOCUS/Fstream.thy FOCUS/FOCUS.thy \ - FOCUS/Stream_adm.thy ../Library/Continuity.thy \ - FOCUS/Buffer.thy FOCUS/Buffer_adm.thy - @$(ISABELLE_TOOL) usedir $(OUT)/HOLCF FOCUS - -## IOA - -IOA: HOLCF $(OUT)/IOA - -$(OUT)/IOA: $(OUT)/HOLCF IOA/ROOT.ML IOA/meta_theory/Traces.thy \ - IOA/meta_theory/Asig.thy IOA/meta_theory/CompoScheds.thy \ - IOA/meta_theory/CompoTraces.thy IOA/meta_theory/Seq.thy \ - IOA/meta_theory/RefCorrectness.thy IOA/meta_theory/Automata.thy \ - IOA/meta_theory/ShortExecutions.thy IOA/meta_theory/IOA.thy \ - IOA/meta_theory/Sequence.thy IOA/meta_theory/CompoExecs.thy \ - IOA/meta_theory/RefMappings.thy IOA/meta_theory/Compositionality.thy \ - IOA/meta_theory/TL.thy IOA/meta_theory/TLS.thy \ - IOA/meta_theory/LiveIOA.thy IOA/meta_theory/Pred.thy \ - IOA/meta_theory/Abstraction.thy IOA/meta_theory/Simulations.thy \ - IOA/meta_theory/SimCorrectness.thy - @cd IOA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOLCF IOA - - -## IOA-ABP - -IOA-ABP: IOA $(LOG)/IOA-ABP.gz - -$(LOG)/IOA-ABP.gz: $(OUT)/IOA IOA/ABP/Abschannel.thy \ - IOA/ABP/Abschannel_finite.thy IOA/ABP/Action.thy \ - IOA/ABP/Check.ML IOA/ABP/Correctness.thy \ - IOA/ABP/Env.thy IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy \ - IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \ - IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy IOA/ABP/Sender.thy \ - IOA/ABP/Spec.thy - @cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ABP - -## IOA-NTP - -IOA-NTP: IOA $(LOG)/IOA-NTP.gz - -$(LOG)/IOA-NTP.gz: $(OUT)/IOA \ - IOA/NTP/Abschannel.thy IOA/NTP/Action.thy IOA/NTP/Correctness.thy \ - IOA/NTP/Impl.thy IOA/NTP/Lemmas.thy IOA/NTP/Multiset.thy \ - IOA/NTP/Packet.thy IOA/NTP/ROOT.ML IOA/NTP/Receiver.thy IOA/NTP/Sender.thy \ - IOA/NTP/Spec.thy - @cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA NTP - - -## IOA-Storage - -IOA-Storage: IOA $(LOG)/IOA-Storage.gz - -$(LOG)/IOA-Storage.gz: $(OUT)/IOA IOA/Storage/Action.thy \ - IOA/Storage/Correctness.thy IOA/Storage/Impl.thy \ - IOA/Storage/ROOT.ML IOA/Storage/Spec.thy - @cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA Storage - - -## IOA-ex - -IOA-ex: IOA $(LOG)/IOA-ex.gz - -$(LOG)/IOA-ex.gz: $(OUT)/IOA IOA/ex/ROOT.ML IOA/ex/TrivEx.thy IOA/ex/TrivEx2.thy - @cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ex - - -## clean - -clean: - @rm -f $(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz \ - $(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA \ - $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz \ - $(LOG)/IOA-Storage.gz $(LOG)/HOLCF-Library.gz \ - $(LOG)/IOA-ex.gz $(LOG)/HOLCF-Tutorial.gz diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/HOLCF/Library/ROOT.ML --- a/src/HOL/HOLCF/Library/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -use_thys ["HOLCF_Library"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/HOLCF/ROOT.ML --- a/src/HOL/HOLCF/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -(* Title: HOL/HOLCF/ROOT.ML - Author: Franz Regensburger - -HOLCF -- a semantic extension of HOL by the LCF logic. -*) - -no_document use_thys ["~~/src/HOL/Library/Nat_Bijection", "~~/src/HOL/Library/Countable"]; - -use_thys ["Plain_HOLCF", "Fixrec", "HOLCF"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/HOLCF/Tutorial/ROOT.ML --- a/src/HOL/HOLCF/Tutorial/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -use_thys ["Domain_ex", "Fixrec_ex", "New_Domain"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/HOLCF/ex/ROOT.ML --- a/src/HOL/HOLCF/ex/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,10 +0,0 @@ -(* Title: HOL/HOLCF/ex/ROOT.ML - -Misc HOLCF examples. -*) - -use_thys ["Dnat", "Dagstuhl", "Focus_ex", "Fix2", "Hoare", - "Concurrency_Monad", - "Loop", "Powerdomain_ex", "Domain_Proofs", - "Letrec", - "Pattern_Match"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Hahn_Banach/ROOT.ML --- a/src/HOL/Hahn_Banach/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ -(* Title: HOL/Hahn_Banach/ROOT.ML - Author: Gertrud Bauer, TU Munich - -The Hahn-Banach theorem for real vector spaces (Isabelle/Isar). -*) - -use_thys ["Hahn_Banach"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Hoare/ROOT.ML --- a/src/HOL/Hoare/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2 +0,0 @@ - -use_thy "Hoare"; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Hoare_Parallel/ROOT.ML --- a/src/HOL/Hoare_Parallel/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -use_thys ["Hoare_Parallel"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/IMP/ROOT.ML --- a/src/HOL/IMP/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,39 +0,0 @@ -no_document use_thys - ["~~/src/HOL/ex/Interpretation_with_Defs", - "~~/src/HOL/Library/While_Combinator", - "~~/src/HOL/Library/Char_ord", "~~/src/HOL/Library/List_lexord" - ]; - -use_thys -["BExp", - "ASM", - "Small_Step", - "Denotation", - "Comp_Rev", - "Poly_Types", - "Sec_Typing", - "Sec_TypingT", - "Def_Ass_Sound_Big", - "Def_Ass_Sound_Small", - "Live", - "Live_True", - "Hoare_Examples", - "VC", - "HoareT", - "Collecting1", - "Collecting_list", - "Abs_Int_Tests", - "Abs_Int1_parity", - "Abs_Int1_const", - "Abs_Int3", - "Abs_Int_ITP/Abs_Int1_parity_ITP", - "Abs_Int_ITP/Abs_Int1_const_ITP", - "Abs_Int_ITP/Abs_Int3_ITP", - "Abs_Int_Den/Abs_Int_den2", - "Procs_Dyn_Vars_Dyn", - "Procs_Stat_Vars_Dyn", - "Procs_Stat_Vars_Stat", - "C_like", - "OO", - "Fold" -]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/IMPP/ROOT.ML --- a/src/HOL/IMPP/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,6 +0,0 @@ -(* Title: HOL/IMPP/ROOT.ML - Author: David von Oheimb - Copyright 1999 TUM -*) - -use_thys ["EvenOdd"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/IOA/ROOT.ML --- a/src/HOL/IOA/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,27 +0,0 @@ -(* Title: HOL/IOA/ROOT.ML - Author: Tobias Nipkow & Konrad Slind - Copyright 1994 TU Muenchen - -This is the ROOT file for the meta theory of I/O-Automata. - -@inproceedings{Nipkow-Slind-IOA, -author={Tobias Nipkow and Konrad Slind}, -title={{I/O} Automata in {Isabelle/HOL}}, -booktitle={Proc.\ TYPES Workshop 1994}, -publisher=Springer, -series=LNCS, -note={To appear}} -ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz - -and - -@inproceedings{Mueller-Nipkow, -author={Olaf M\"uller and Tobias Nipkow}, -title={Combining Model Checking and Deduction for {I/O}-Automata}, -booktitle={Proc.\ TACAS Workshop}, -organization={Aarhus University, BRICS report}, -year=1995} -ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz -*) - -use_thys ["Solve"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Imperative_HOL/ROOT.ML --- a/src/HOL/Imperative_HOL/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ -no_document use_thys [ - "~~/src/HOL/Library/Countable", - "~~/src/HOL/Library/Monad_Syntax", - "~~/src/HOL/Library/Code_Natural", - "~~/src/HOL/Library/LaTeXsugar"]; - -use_thys ["Imperative_HOL_ex"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Import/ROOT.ML --- a/src/HOL/Import/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,5 +0,0 @@ -use_thy "HOL_Light_Maps"; - -if getenv "HOL_LIGHT_BUNDLE" <> "" -then use_thy "HOL_Light_Import" -else () diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Induct/ROOT.ML --- a/src/HOL/Induct/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,5 +0,0 @@ -Unsynchronized.setmp quick_and_dirty true - use_thys ["Common_Patterns"]; - -use_thys ["QuoDataType", "QuoNestedDataType", "Term", "SList", - "ABexp", "Tree", "Ordinals", "Sigma_Algebra", "Comb", "PropLog", "Com"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Aug 07 23:38:18 2012 +0200 +++ b/src/HOL/IsaMakefile Tue Aug 07 23:43:05 2012 +0200 @@ -1,1883 +1,36 @@ -# -# IsaMakefile for HOL # - -## targets +# approximative IsaMakefile for legacy applications +# default: HOL -images: \ - HOL \ - HOL-Library \ - HOL-Algebra \ - HOL-Boogie \ - HOL-IMP \ - HOL-Multivariate_Analysis \ - HOL-NSA \ - HOL-Nominal \ - HOL-Proofs \ - HOL-SPARK \ - HOL-Word \ - HOLCF \ - IOA \ - TLA \ - HOL-Base \ - HOL-Main \ - HOL-Plain +clean: + -@$(ISABELLE_TOOL) build -a -n -c -#Note: keep targets sorted -test: \ - HOL-Auth \ - HOL-Bali \ - HOL-Boogie-Examples \ - HOL-Hahn_Banach \ - HOL-Hoare \ - HOL-Hoare_Parallel \ - HOLCF-FOCUS \ - HOLCF-IMP \ - HOLCF-Library \ - HOLCF-Tutorial \ - HOLCF-ex \ - HOL-IMPP \ - HOL-Import \ - HOL-IOA \ - IOA-ABP \ - IOA-NTP \ - IOA-Storage \ - IOA-ex \ - HOL-Imperative_HOL \ - HOL-Induct \ - HOL-Isar_Examples \ - HOL-Lattice \ - HOL-Library-Codegenerator_Test \ - HOL-Matrix_LP \ - HOL-Metis_Examples \ - HOL-MicroJava \ - HOL-Mirabelle \ - HOL-Mutabelle \ - HOL-NanoJava \ - HOL-Nitpick_Examples \ - HOL-NSA-Examples \ - HOL-Number_Theory \ - HOL-Old_Number_Theory \ - HOL-Quickcheck_Examples \ - HOL-Quotient_Examples \ - HOL-Predicate_Compile_Examples \ - HOL-Prolog \ - HOL-Proofs-ex \ - HOL-Proofs-Lambda \ - HOL-SET_Protocol \ - HOL-SPARK-Examples \ - HOL-SPARK-Manual \ - HOL-Word-SMT_Examples \ - HOL-Statespace \ - TLA-Buffer \ - TLA-Inc \ - TLA-Memory \ - HOL-TPTP \ - HOL-UNITY \ - HOL-Unix \ - HOL-Word-Examples \ - HOL-ZF - # ^ this is the sort position - -benchmark: \ - HOL-Datatype_Benchmark \ - HOL-Quickcheck_Benchmark \ - HOL-Record_Benchmark - -images-no-smlnj: \ - HOL-Probability - -test-no-smlnj: \ - HOL-ex \ - HOL-Decision_Procs \ - HOL-Proofs-Extraction \ - HOL-Nominal-Examples - -all: test-no-smlnj test images-no-smlnj images -full: all benchmark -smlnj: test images - - -## global settings - -SRC = $(ISABELLE_HOME)/src -OUT = $(ISABELLE_OUTPUT) -LOG = $(OUT)/log - - -## HOL - -HOL: Pure $(OUT)/HOL - -HOL-Base: Pure $(OUT)/HOL-Base - -HOL-Plain: Pure $(OUT)/HOL-Plain - -HOL-Main: Pure $(OUT)/HOL-Main +all: + @$(ISABELLE_TOOL) build -a Pure: - @cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure - -$(OUT)/Pure: Pure - -BASE_DEPENDENCIES = $(OUT)/Pure \ - $(SRC)/Provers/blast.ML \ - $(SRC)/Provers/clasimp.ML \ - $(SRC)/Provers/classical.ML \ - $(SRC)/Provers/hypsubst.ML \ - $(SRC)/Provers/quantifier1.ML \ - $(SRC)/Provers/splitter.ML \ - $(SRC)/Tools/Code/code_haskell.ML \ - $(SRC)/Tools/Code/code_ml.ML \ - $(SRC)/Tools/Code/code_namespace.ML \ - $(SRC)/Tools/Code/code_preproc.ML \ - $(SRC)/Tools/Code/code_printer.ML \ - $(SRC)/Tools/Code/code_runtime.ML \ - $(SRC)/Tools/Code/code_scala.ML \ - $(SRC)/Tools/Code/code_simp.ML \ - $(SRC)/Tools/Code/code_target.ML \ - $(SRC)/Tools/Code/code_thingol.ML \ - $(SRC)/Tools/Code_Generator.thy \ - $(SRC)/Tools/IsaPlanner/isand.ML \ - $(SRC)/Tools/IsaPlanner/rw_inst.ML \ - $(SRC)/Tools/IsaPlanner/rw_tools.ML \ - $(SRC)/Tools/IsaPlanner/zipper.ML \ - $(SRC)/Tools/atomize_elim.ML \ - $(SRC)/Tools/cache_io.ML \ - $(SRC)/Tools/case_product.ML \ - $(SRC)/Tools/coherent.ML \ - $(SRC)/Tools/cong_tac.ML \ - $(SRC)/Tools/eqsubst.ML \ - $(SRC)/Tools/induct.ML \ - $(SRC)/Tools/induct_tacs.ML \ - $(SRC)/Tools/induction.ML \ - $(SRC)/Tools/intuitionistic.ML \ - $(SRC)/Tools/misc_legacy.ML \ - $(SRC)/Tools/nbe.ML \ - $(SRC)/Tools/project_rule.ML \ - $(SRC)/Tools/quickcheck.ML \ - $(SRC)/Tools/solve_direct.ML \ - $(SRC)/Tools/subtyping.ML \ - $(SRC)/Tools/try.ML \ - $(SRC)/Tools/value.ML \ - HOL.thy \ - Tools/hologic.ML \ - Tools/simpdata.ML - -$(OUT)/HOL-Base: base.ML $(BASE_DEPENDENCIES) - @$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base - -PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES) \ - $(SRC)/Provers/Arith/cancel_div_mod.ML \ - $(SRC)/Provers/Arith/fast_lin_arith.ML \ - $(SRC)/Provers/order.ML \ - $(SRC)/Provers/trancl.ML \ - $(SRC)/Tools/Metis/metis.ML \ - $(SRC)/Tools/rat.ML \ - ATP.thy \ - Complete_Lattices.thy \ - Complete_Partial_Order.thy \ - Datatype.thy \ - Extraction.thy \ - Fields.thy \ - Finite_Set.thy \ - Fun.thy \ - FunDef.thy \ - Groups.thy \ - Inductive.thy \ - Lattices.thy \ - Meson.thy \ - Metis.thy \ - Nat.thy \ - Num.thy \ - Option.thy \ - Orderings.thy \ - Partial_Function.thy \ - Plain.thy \ - Power.thy \ - Product_Type.thy \ - Relation.thy \ - Rings.thy \ - SAT.thy \ - Set.thy \ - Sum_Type.thy \ - Tools/ATP/atp_problem.ML \ - Tools/ATP/atp_problem_generate.ML \ - Tools/ATP/atp_proof.ML \ - Tools/ATP/atp_proof_reconstruct.ML \ - Tools/ATP/atp_proof_redirect.ML \ - Tools/ATP/atp_systems.ML \ - Tools/ATP/atp_util.ML \ - Tools/Datatype/datatype.ML \ - Tools/Datatype/datatype_aux.ML \ - Tools/Datatype/datatype_case.ML \ - Tools/Datatype/datatype_codegen.ML \ - Tools/Datatype/datatype_data.ML \ - Tools/Datatype/datatype_prop.ML \ - Tools/Datatype/datatype_realizer.ML \ - Tools/Datatype/primrec.ML \ - Tools/Datatype/rep_datatype.ML \ - Tools/Function/context_tree.ML \ - Tools/Function/fun.ML \ - Tools/Function/function.ML \ - Tools/Function/function_common.ML \ - Tools/Function/function_core.ML \ - Tools/Function/function_lib.ML \ - Tools/Function/induction_schema.ML \ - Tools/Function/lexicographic_order.ML \ - Tools/Function/measure_functions.ML \ - Tools/Function/mutual.ML \ - Tools/Function/partial_function.ML \ - Tools/Function/pat_completeness.ML \ - Tools/Function/pattern_split.ML \ - Tools/Function/relation.ML \ - Tools/Function/scnp_reconstruct.ML \ - Tools/Function/scnp_solve.ML \ - Tools/Function/size.ML \ - Tools/Function/sum_tree.ML \ - Tools/Function/termination.ML \ - Tools/Meson/meson.ML \ - Tools/Meson/meson_clausify.ML \ - Tools/Meson/meson_tactic.ML \ - Tools/Metis/metis_generate.ML \ - Tools/Metis/metis_reconstruct.ML \ - Tools/Metis/metis_tactic.ML \ - Tools/arith_data.ML \ - Tools/cnf_funcs.ML \ - Tools/enriched_type.ML \ - Tools/group_cancel.ML \ - Tools/inductive.ML \ - Tools/inductive_realizer.ML \ - Tools/inductive_set.ML \ - Tools/lambda_lifting.ML \ - Tools/lin_arith.ML \ - Tools/monomorph.ML \ - Tools/nat_arith.ML \ - Tools/prop_logic.ML \ - Tools/refute.ML \ - Tools/rewrite_hol_proof.ML \ - Tools/sat_funcs.ML \ - Tools/sat_solver.ML \ - Tools/set_comprehension_pointfree.ML \ - Tools/split_rule.ML \ - Tools/try0.ML \ - Tools/typedef.ML \ - Transitive_Closure.thy \ - Typedef.thy \ - Wellfounded.thy - -$(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES) - @$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain + @$(ISABELLE_TOOL) build -b Pure -MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \ - Big_Operators.thy \ - Code_Evaluation.thy \ - Code_Numeral.thy \ - Divides.thy \ - DSequence.thy \ - Equiv_Relations.thy \ - Enum.thy \ - Groebner_Basis.thy \ - Hilbert_Choice.thy \ - Int.thy \ - Lazy_Sequence.thy \ - Lifting.thy \ - List.thy \ - Main.thy \ - Map.thy \ - Nat_Transfer.thy \ - New_DSequence.thy \ - New_Random_Sequence.thy \ - Nitpick.thy \ - Numeral_Simprocs.thy \ - Presburger.thy \ - Predicate.thy \ - Predicate_Compile.thy \ - Quickcheck.thy \ - Quickcheck_Exhaustive.thy \ - Quickcheck_Narrowing.thy \ - Quotient.thy \ - Random.thy \ - Random_Sequence.thy \ - Record.thy \ - Refute.thy \ - Semiring_Normalization.thy \ - Set_Interval.thy \ - Sledgehammer.thy \ - SMT.thy \ - String.thy \ - Transfer.thy \ - Typerep.thy \ - $(SRC)/Provers/Arith/assoc_fold.ML \ - $(SRC)/Provers/Arith/cancel_numeral_factor.ML \ - $(SRC)/Provers/Arith/cancel_numerals.ML \ - $(SRC)/Provers/Arith/combine_numerals.ML \ - $(SRC)/Provers/Arith/extract_common_term.ML \ - Tools/choice_specification.ML \ - Tools/code_evaluation.ML \ - Tools/groebner.ML \ - Tools/int_arith.ML \ - Tools/legacy_transfer.ML \ - Tools/Lifting/lifting_def.ML \ - Tools/Lifting/lifting_info.ML \ - Tools/Lifting/lifting_term.ML \ - Tools/Lifting/lifting_setup.ML \ - Tools/list_code.ML \ - Tools/list_to_set_comprehension.ML \ - Tools/nat_numeral_simprocs.ML \ - Tools/Nitpick/kodkod.ML \ - Tools/Nitpick/kodkod_sat.ML \ - Tools/Nitpick/nitpick.ML \ - Tools/Nitpick/nitpick_hol.ML \ - Tools/Nitpick/nitpick_isar.ML \ - Tools/Nitpick/nitpick_kodkod.ML \ - Tools/Nitpick/nitpick_model.ML \ - Tools/Nitpick/nitpick_mono.ML \ - Tools/Nitpick/nitpick_nut.ML \ - Tools/Nitpick/nitpick_peephole.ML \ - Tools/Nitpick/nitpick_preproc.ML \ - Tools/Nitpick/nitpick_rep.ML \ - Tools/Nitpick/nitpick_scope.ML \ - Tools/Nitpick/nitpick_tests.ML \ - Tools/Nitpick/nitpick_util.ML \ - Tools/numeral.ML \ - Tools/numeral_simprocs.ML \ - Tools/Predicate_Compile/core_data.ML \ - Tools/Predicate_Compile/mode_inference.ML \ - Tools/Predicate_Compile/predicate_compile_aux.ML \ - Tools/Predicate_Compile/predicate_compile_compilations.ML \ - Tools/Predicate_Compile/predicate_compile_core.ML \ - Tools/Predicate_Compile/predicate_compile_data.ML \ - Tools/Predicate_Compile/predicate_compile_fun.ML \ - Tools/Predicate_Compile/predicate_compile.ML \ - Tools/Predicate_Compile/predicate_compile_proof.ML \ - Tools/Predicate_Compile/predicate_compile_specialisation.ML \ - Tools/Predicate_Compile/predicate_compile_pred.ML \ - Tools/Qelim/cooper.ML \ - Tools/Qelim/cooper_procedure.ML \ - Tools/Qelim/qelim.ML \ - Tools/Quickcheck/exhaustive_generators.ML \ - Tools/Quickcheck/random_generators.ML \ - Tools/Quickcheck/quickcheck_common.ML \ - Tools/Quickcheck/narrowing_generators.ML \ - Tools/Quickcheck/Narrowing_Engine.hs \ - Tools/Quickcheck/PNF_Narrowing_Engine.hs \ - Tools/Quotient/quotient_def.ML \ - Tools/Quotient/quotient_info.ML \ - Tools/Quotient/quotient_tacs.ML \ - Tools/Quotient/quotient_term.ML \ - Tools/Quotient/quotient_type.ML \ - Tools/record.ML \ - Tools/semiring_normalizer.ML \ - Tools/Sledgehammer/async_manager.ML \ - Tools/Sledgehammer/sledgehammer_fact.ML \ - Tools/Sledgehammer/sledgehammer_mash.ML \ - Tools/Sledgehammer/sledgehammer_mepo.ML \ - Tools/Sledgehammer/sledgehammer_minimize.ML \ - Tools/Sledgehammer/sledgehammer_isar.ML \ - Tools/Sledgehammer/sledgehammer_provers.ML \ - Tools/Sledgehammer/sledgehammer_run.ML \ - Tools/Sledgehammer/sledgehammer_util.ML \ - Tools/SMT/smtlib_interface.ML \ - Tools/SMT/smt_builtin.ML \ - Tools/SMT/smt_config.ML \ - Tools/SMT/smt_datatypes.ML \ - Tools/SMT/smt_failure.ML \ - Tools/SMT/smt_normalize.ML \ - Tools/SMT/smt_setup_solvers.ML \ - Tools/SMT/smt_solver.ML \ - Tools/SMT/smt_translate.ML \ - Tools/SMT/smt_utils.ML \ - Tools/SMT/z3_interface.ML \ - Tools/SMT/z3_model.ML \ - Tools/SMT/z3_proof_literals.ML \ - Tools/SMT/z3_proof_methods.ML \ - Tools/SMT/z3_proof_parser.ML \ - Tools/SMT/z3_proof_reconstruction.ML \ - Tools/SMT/z3_proof_tools.ML \ - Tools/string_code.ML \ - Tools/string_syntax.ML \ - Tools/transfer.ML \ - -$(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES) - @$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main - -HOL_DEPENDENCIES = $(MAIN_DEPENDENCIES) \ - Archimedean_Field.thy \ - Complex.thy \ - Complex_Main.thy \ - Deriv.thy \ - Fact.thy \ - GCD.thy \ - Lim.thy \ - Limits.thy \ - Ln.thy \ - Log.thy \ - Lubs.thy \ - MacLaurin.thy \ - NthRoot.thy \ - Parity.thy \ - RComplete.thy \ - Rat.thy \ - Real.thy \ - RealDef.thy \ - RealVector.thy \ - SEQ.thy \ - Series.thy \ - SupInf.thy \ - Taylor.thy \ - Tools/SMT/smt_real.ML \ - Tools/float_syntax.ML \ - Transcendental.thy - -$(OUT)/HOL: ROOT.ML $(HOL_DEPENDENCIES) - @$(ISABELLE_TOOL) usedir -b -g true $(OUT)/Pure HOL - - -## HOL-Library - -HOL-Library: HOL $(OUT)/HOL-Library - -$(OUT)/HOL-Library: $(OUT)/HOL Library/ROOT.ML \ - $(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML \ - Library/Abstract_Rat.thy $(SRC)/Tools/Adhoc_Overloading.thy \ - Library/AList.thy Library/AList_Mapping.thy \ - Library/BigO.thy Library/Binomial.thy \ - Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy \ - Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy \ - Library/Code_Char_ord.thy Library/Code_Integer.thy \ - Library/Code_Nat.thy Library/Code_Natural.thy \ - Library/Efficient_Nat.thy Library/Code_Prolog.thy \ - Library/Code_Real_Approx_By_Float.thy \ - Tools/Predicate_Compile/code_prolog.ML Library/ContNotDenum.thy \ - Library/Continuity.thy \ - Library/Convex.thy Library/Countable.thy \ - Library/Debug.thy \ - Library/Dlist.thy Library/Eval_Witness.thy \ - Library/DAList.thy Library/Dlist.thy \ - Library/Eval_Witness.thy \ - Library/Extended_Real.thy Library/Extended_Nat.thy \ - Library/FinFun.thy Library/FinFun_Syntax.thy Library/Float.thy \ - Library/Formal_Power_Series.thy Library/Fraction_Field.thy \ - Library/FrechetDeriv.thy Library/FuncSet.thy \ - Library/Function_Algebras.thy Library/Function_Division.thy \ - Library/Fundamental_Theorem_Algebra.thy \ - Library/Glbs.thy Library/Indicator_Function.thy \ - Library/Infinite_Set.thy Library/Inner_Product.thy \ - Library/Kleene_Algebra.thy Library/LaTeXsugar.thy \ - Library/Lattice_Algebras.thy Library/Lattice_Syntax.thy \ - Library/Library.thy Library/List_Prefix.thy \ - Library/List_lexord.thy Library/Mapping.thy Library/Monad_Syntax.thy \ - Library/Multiset.thy Library/Nat_Bijection.thy \ - Library/Numeral_Type.thy Library/Old_Recdef.thy \ - Library/OptionalSugar.thy Library/Order_Relation.thy \ - Library/Parallel.thy \ - Library/Permutation.thy Library/Permutations.thy \ - Library/Phantom_Type.thy Library/Poly_Deriv.thy \ - Library/Polynomial.thy Library/Predicate_Compile_Quickcheck.thy \ - Library/Preorder.thy Library/Product_Vector.thy \ - Library/Product_ord.thy Library/Product_plus.thy \ - Library/Product_Lattice.thy Library/Quickcheck_Types.thy \ - Library/Quotient_List.thy Library/Quotient_Option.thy \ - Library/Quotient_Product.thy Library/Quotient_Set.thy \ - Library/Quotient_Sum.thy Library/Quotient_Syntax.thy \ - Library/Quotient_Type.thy Library/RBT.thy Library/RBT_Impl.thy \ - Library/RBT_Mapping.thy Library/README.html Library/Saturated.thy \ - Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy \ - Library/Reflection.thy Library/Sublist_Order.thy \ - Library/Sum_of_Squares.thy Library/Sum_of_Squares/sos_wrapper.ML \ - Library/Sum_of_Squares/sum_of_squares.ML Library/Target_Numeral.thy \ - Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy \ - Library/Wfrec.thy Library/While_Combinator.thy Library/Zorn.thy \ - $(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML \ - Library/reflection.ML Library/reify_data.ML \ - Library/document/root.bib Library/document/root.tex \ - Tools/TFL/casesplit.ML Tools/TFL/dcterm.ML Tools/TFL/post.ML \ - Tools/TFL/rules.ML Tools/TFL/tfl.ML Tools/TFL/thms.ML \ - Tools/TFL/thry.ML Tools/TFL/usyntax.ML Tools/TFL/utils.ML \ - Tools/recdef.ML - @cd Library; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL-Library - - -## HOL-Hahn_Banach - -HOL-Hahn_Banach: HOL $(LOG)/HOL-Hahn_Banach.gz - -$(LOG)/HOL-Hahn_Banach.gz: $(OUT)/HOL Hahn_Banach/Bounds.thy \ - Hahn_Banach/Function_Norm.thy Hahn_Banach/Function_Order.thy \ - Hahn_Banach/Hahn_Banach.thy Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy \ - Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Hahn_Banach/Linearform.thy \ - Hahn_Banach/Normed_Space.thy Hahn_Banach/README.html \ - Hahn_Banach/ROOT.ML Hahn_Banach/Subspace.thy \ - Hahn_Banach/Vector_Space.thy Hahn_Banach/Zorn_Lemma.thy \ - Hahn_Banach/document/root.bib Hahn_Banach/document/root.tex - @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hahn_Banach - - -## HOL-Induct - -HOL-Induct: HOL $(LOG)/HOL-Induct.gz - -$(LOG)/HOL-Induct.gz: $(OUT)/HOL Induct/Com.thy Induct/Comb.thy \ - Induct/Ordinals.thy Induct/PropLog.thy Induct/QuoNestedDataType.thy \ - Induct/QuoDataType.thy Induct/ROOT.ML Induct/Sexp.thy \ - Induct/Sigma_Algebra.thy Induct/ABexp.thy Induct/SList.thy \ - Induct/Term.thy Induct/Tree.thy Induct/document/root.tex - @$(ISABELLE_TOOL) usedir $(OUT)/HOL Induct - - -## HOL-IMP - -HOL-IMP: HOL $(OUT)/HOL-IMP +HOL: + @$(ISABELLE_TOOL) build -b HOL -$(OUT)/HOL-IMP: $(OUT)/HOL \ - IMP/ACom.thy \ - IMP/Abs_Int0.thy IMP/Abs_State.thy IMP/Abs_Int1.thy \ - IMP/Abs_Int1_const.thy IMP/Abs_Int1_parity.thy \ - IMP/Abs_Int2.thy IMP/Abs_Int2_ivl.thy IMP/Abs_Int3.thy \ - IMP/Abs_Int_ITP/Abs_Int0_ITP.thy IMP/Abs_Int_ITP/Abs_State_ITP.thy \ - IMP/Abs_Int_ITP/Abs_Int1_ITP.thy IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy \ - IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy IMP/Abs_Int_ITP/Abs_Int2_ITP.thy \ - IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy IMP/Abs_Int_ITP/Abs_Int3_ITP.thy \ - IMP/Abs_Int_Den/Abs_Int_den0_fun.thy \ - IMP/Abs_Int_Den/Abs_State_den.thy IMP/Abs_Int_Den/Abs_Int_den0.thy \ - IMP/Abs_Int_Den/Abs_Int_den0_const.thy IMP/Abs_Int_Den/Abs_Int_den1.thy \ - IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy IMP/Abs_Int_Den/Abs_Int_den2.thy \ - IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy IMP/Big_Step.thy IMP/C_like.thy \ - IMP/Collecting.thy IMP/Collecting_list.thy IMP/Collecting1.thy IMP/Com.thy \ - IMP/Compiler.thy IMP/Comp_Rev.thy \ - IMP/Def_Ass.thy IMP/Def_Ass_Big.thy IMP/Def_Ass_Exp.thy \ - IMP/Def_Ass_Small.thy IMP/Def_Ass_Sound_Big.thy \ - IMP/Def_Ass_Sound_Small.thy IMP/Denotation.thy IMP/Hoare.thy \ - IMP/HoareT.thy IMP/Hoare_Examples.thy IMP/Hoare_Sound_Complete.thy \ - IMP/Live.thy IMP/Live_True.thy IMP/OO.thy IMP/Poly_Types.thy IMP/Procs.thy \ - IMP/Procs_Dyn_Vars_Dyn.thy IMP/Procs_Stat_Vars_Dyn.thy \ - IMP/Procs_Stat_Vars_Stat.thy IMP/Sec_Type_Expr.thy IMP/Sec_Typing.thy \ - IMP/Sec_TypingT.thy IMP/Small_Step.thy IMP/Star.thy IMP/Types.thy \ - IMP/VC.thy IMP/Vars.thy \ - IMP/ROOT.ML IMP/document/root.tex IMP/document/root.bib - @cd IMP && $(ISABELLE_TOOL) usedir -g true -b $(OUT)/HOL HOL-IMP - -## HOL-IMPP - -HOL-IMPP: HOL $(LOG)/HOL-IMPP.gz - -$(LOG)/HOL-IMPP.gz: $(OUT)/HOL IMPP/ROOT.ML IMPP/Com.thy \ - IMPP/Natural.thy IMPP/Hoare.thy IMPP/Misc.thy IMPP/EvenOdd.thy - @$(ISABELLE_TOOL) usedir $(OUT)/HOL IMPP - - -## HOL-Import - -HOL-Import: $(LOG)/HOL-Import.gz - -$(LOG)/HOL-Import.gz: $(OUT)/HOL \ - Import/ROOT.ML \ - Import/Import_Setup.thy \ - Import/import_data.ML \ - Import/import_rule.ML \ - Import/HOL_Light_Maps.thy \ - Import/HOL_Light_Import.thy - @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Import - - -## HOL-Number_Theory - -HOL-Number_Theory: HOL $(LOG)/HOL-Number_Theory.gz - -$(LOG)/HOL-Number_Theory.gz: $(OUT)/HOL $(ALGEBRA_DEPENDENCIES) \ - Library/Multiset.thy \ - Number_Theory/Binomial.thy \ - Number_Theory/Cong.thy \ - Number_Theory/Fib.thy \ - Number_Theory/MiscAlgebra.thy \ - Number_Theory/Number_Theory.thy \ - Number_Theory/Residues.thy \ - Number_Theory/UniqueFactorization.thy \ - Number_Theory/ROOT.ML - @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Number_Theory - - -## HOL-Old_Number_Theory - -HOL-Old_Number_Theory: HOL $(LOG)/HOL-Old_Number_Theory.gz - -$(LOG)/HOL-Old_Number_Theory.gz: $(OUT)/HOL Library/Permutation.thy \ - Old_Number_Theory/Primes.thy Old_Number_Theory/Fib.thy \ - Old_Number_Theory/Factorization.thy Old_Number_Theory/BijectionRel.thy\ - Old_Number_Theory/Chinese.thy Old_Number_Theory/EulerFermat.thy \ - Old_Number_Theory/IntFact.thy Old_Number_Theory/IntPrimes.thy \ - Old_Number_Theory/WilsonBij.thy Old_Number_Theory/WilsonRuss.thy \ - Old_Number_Theory/Finite2.thy Old_Number_Theory/Int2.thy \ - Old_Number_Theory/EvenOdd.thy Old_Number_Theory/Residues.thy \ - Old_Number_Theory/Euler.thy Old_Number_Theory/Gauss.thy \ - Old_Number_Theory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy \ - Old_Number_Theory/Legacy_GCD.thy Old_Number_Theory/Pocklington.thy \ - Old_Number_Theory/ROOT.ML - @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Old_Number_Theory - - -## HOL-Hoare - -HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz - -$(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.thy Hoare/Examples.thy \ - Hoare/Hoare.thy Hoare/hoare_syntax.ML Hoare/hoare_tac.ML \ - Hoare/Heap.thy Hoare/Hoare_Logic.thy Hoare/Hoare_Logic_Abort.thy \ - Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy Hoare/ROOT.ML \ - Hoare/ExamplesAbort.thy Hoare/HeapSyntaxAbort.thy \ - Hoare/SchorrWaite.thy Hoare/Separation.thy Hoare/SepLogHeap.thy \ - Hoare/document/root.tex Hoare/document/root.bib - @$(ISABELLE_TOOL) usedir $(OUT)/HOL Hoare - - -## HOL-Hoare_Parallel - -HOL-Hoare_Parallel: HOL $(LOG)/HOL-Hoare_Parallel.gz - -$(LOG)/HOL-Hoare_Parallel.gz: $(OUT)/HOL Hoare_Parallel/Gar_Coll.thy \ - Hoare_Parallel/Graph.thy Hoare_Parallel/Hoare_Parallel.thy \ - Hoare_Parallel/Mul_Gar_Coll.thy Hoare_Parallel/OG_Com.thy \ - Hoare_Parallel/OG_Examples.thy Hoare_Parallel/OG_Hoare.thy \ - Hoare_Parallel/OG_Syntax.thy Hoare_Parallel/OG_Tactics.thy \ - Hoare_Parallel/OG_Tran.thy Hoare_Parallel/Quote_Antiquote.thy \ - Hoare_Parallel/RG_Com.thy Hoare_Parallel/RG_Examples.thy \ - Hoare_Parallel/RG_Hoare.thy Hoare_Parallel/RG_Syntax.thy \ - Hoare_Parallel/RG_Tran.thy Hoare_Parallel/ROOT.ML \ - Hoare_Parallel/document/root.tex Hoare_Parallel/document/root.bib - @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hoare_Parallel - - -## HOL-Library-Codegenerator_Test - -HOL-Library-Codegenerator_Test: HOL-Library $(LOG)/HOL-Library-Codegenerator_Test.gz - -$(LOG)/HOL-Library-Codegenerator_Test.gz: $(OUT)/HOL-Library \ - Codegenerator_Test/ROOT.ML \ - Codegenerator_Test/Candidates.thy \ - Codegenerator_Test/Candidates_Pretty.thy \ - Codegenerator_Test/Generate.thy \ - Codegenerator_Test/Generate_Pretty.thy - @$(ISABELLE_TOOL) usedir -d false -g false -i false $(OUT)/HOL-Library Codegenerator_Test - - -## HOL-Metis_Examples - -HOL-Metis_Examples: HOL $(LOG)/HOL-Metis_Examples.gz - -$(LOG)/HOL-Metis_Examples.gz: $(OUT)/HOL Metis_Examples/ROOT.ML \ - Metis_Examples/Abstraction.thy Metis_Examples/Big_O.thy \ - Metis_Examples/Binary_Tree.thy Metis_Examples/Clausification.thy \ - Metis_Examples/Message.thy Metis_Examples/Proxies.thy \ - Metis_Examples/Sets.thy Metis_Examples/Tarski.thy \ - Metis_Examples/Trans_Closure.thy Metis_Examples/Type_Encodings.thy - @$(ISABELLE_TOOL) usedir $(OUT)/HOL Metis_Examples - - -## HOL-Nitpick_Examples - -HOL-Nitpick_Examples: HOL $(LOG)/HOL-Nitpick_Examples.gz - -$(LOG)/HOL-Nitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML \ - Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy \ - Nitpick_Examples/Hotel_Nits.thy Nitpick_Examples/Induct_Nits.thy \ - Nitpick_Examples/Integer_Nits.thy Nitpick_Examples/Manual_Nits.thy \ - Nitpick_Examples/Mini_Nits.thy Nitpick_Examples/Mono_Nits.thy \ - Nitpick_Examples/Nitpick_Examples.thy Nitpick_Examples/Pattern_Nits.thy \ - Nitpick_Examples/Record_Nits.thy Nitpick_Examples/Refute_Nits.thy \ - Nitpick_Examples/Special_Nits.thy Nitpick_Examples/Tests_Nits.thy \ - Nitpick_Examples/Typedef_Nits.thy Nitpick_Examples/minipick.ML - @$(ISABELLE_TOOL) usedir $(OUT)/HOL Nitpick_Examples - - -## HOL-Algebra - -HOL-Algebra: HOL $(OUT)/HOL-Algebra - -ALGEBRA_DEPENDENCIES = $(OUT)/HOL \ - Algebra/ROOT.ML \ - Library/Binomial.thy \ - Library/FuncSet.thy \ - Library/Multiset.thy \ - Library/Permutation.thy \ - Number_Theory/Primes.thy \ - Algebra/AbelCoset.thy \ - Algebra/Bij.thy \ - Algebra/Congruence.thy \ - Algebra/Coset.thy \ - Algebra/Divisibility.thy \ - Algebra/Exponent.thy \ - Algebra/FiniteProduct.thy \ - Algebra/Group.thy \ - Algebra/Ideal.thy \ - Algebra/IntRing.thy \ - Algebra/Lattice.thy \ - Algebra/Module.thy \ - Algebra/QuotRing.thy \ - Algebra/Ring.thy \ - Algebra/RingHom.thy \ - Algebra/Sylow.thy \ - Algebra/UnivPoly.thy \ - Algebra/abstract/Abstract.thy \ - Algebra/abstract/Factor.thy \ - Algebra/abstract/Field.thy \ - Algebra/abstract/Ideal2.thy \ - Algebra/abstract/PID.thy \ - Algebra/abstract/Ring2.thy \ - Algebra/abstract/RingHomo.thy \ - Algebra/document/root.tex \ - Algebra/document/root.tex \ - Algebra/poly/LongDiv.thy \ - Algebra/poly/PolyHomo.thy \ - Algebra/poly/Polynomial.thy \ - Algebra/poly/UnivPoly2.thy \ - Algebra/ringsimp.ML - -$(OUT)/HOL-Algebra: $(ALGEBRA_DEPENDENCIES) - @cd Algebra; $(ISABELLE_TOOL) usedir -b -g true -V outline=/proof,/ML $(OUT)/HOL HOL-Algebra - - -## HOL-Auth - -HOL-Auth: HOL $(LOG)/HOL-Auth.gz - -$(LOG)/HOL-Auth.gz: $(OUT)/HOL \ - Auth/Auth_Shared.thy Auth/Auth_Public.thy Auth/All_Symmetric.thy \ - Auth/Guard/Auth_Guard_Shared.thy \ - Auth/Guard/Auth_Guard_Public.thy \ - Auth/Smartcard/Auth_Smartcard.thy Auth/All_Symmetric.thy \ - Auth/CertifiedEmail.thy Auth/Event.thy Auth/Message.thy \ - Auth/NS_Public.thy Auth/NS_Public_Bad.thy Auth/NS_Shared.thy \ - Auth/OtwayRees.thy Auth/OtwayReesBella.thy Auth/OtwayRees_AN.thy \ - Auth/OtwayRees_Bad.thy Auth/Public.thy Auth/ROOT.ML Auth/Recur.thy \ - Auth/Shared.thy Auth/TLS.thy Auth/WooLam.thy Auth/Kerberos_BAN.thy \ - Auth/Kerberos_BAN_Gets.thy Auth/KerberosIV.thy \ - Auth/KerberosIV_Gets.thy Auth/KerberosV.thy Auth/Yahalom.thy \ - Auth/Yahalom2.thy Auth/Yahalom_Bad.thy Auth/ZhouGollmann.thy \ - Auth/Guard/Analz.thy Auth/Guard/Extensions.thy Auth/Guard/GuardK.thy \ - Auth/Guard/Guard_Public.thy Auth/Guard/Guard_Shared.thy \ - Auth/Guard/Guard.thy Auth/Guard/List_Msg.thy \ - Auth/Guard/Guard_NS_Public.thy Auth/Guard/Guard_OtwayRees.thy \ - Auth/Guard/P1.thy Auth/Guard/P2.thy Auth/Guard/Proto.thy \ - Auth/Guard/Guard_Yahalom.thy Auth/Smartcard/EventSC.thy \ - Auth/Smartcard/ShoupRubinBella.thy Auth/Smartcard/ShoupRubin.thy \ - Auth/Smartcard/Smartcard.thy Auth/document/root.tex - @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Auth +HOL-Library: + @$(ISABELLE_TOOL) build -b HOL-Library - -## HOL-UNITY - -HOL-UNITY: HOL $(LOG)/HOL-UNITY.gz - -$(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML \ - UNITY/UNITY_Main.thy UNITY/UNITY_tactics.ML UNITY/Comp.thy \ - UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy \ - UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy UNITY/Guar.thy \ - UNITY/Lift_prog.thy UNITY/ListOrder.thy UNITY/ProgressSets.thy \ - UNITY/PPROD.thy UNITY/Project.thy UNITY/Rename.thy \ - UNITY/Transformers.thy UNITY/SubstAx.thy UNITY/UNITY.thy \ - UNITY/Union.thy UNITY/WFair.thy UNITY/Simple/Channel.thy \ - UNITY/Simple/Common.thy UNITY/Simple/Deadlock.thy \ - UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy \ - UNITY/Simple/NSP_Bad.thy UNITY/Simple/Network.thy \ - UNITY/Simple/Reach.thy UNITY/Simple/Reachability.thy \ - UNITY/Simple/Token.thy UNITY/Comp/Alloc.thy UNITY/Comp/AllocBase.thy \ - UNITY/Comp/AllocImpl.thy UNITY/Comp/Client.thy \ - UNITY/Comp/Counter.thy UNITY/Comp/Counterc.thy \ - UNITY/Comp/Handshake.thy UNITY/Comp/PriorityAux.thy \ - UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy \ - UNITY/Comp/TimerArray.thy UNITY/document/root.tex - @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL UNITY - - -## HOL-Unix - -HOL-Unix: HOL $(LOG)/HOL-Unix.gz - -$(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/List_Prefix.thy Unix/ROOT.ML \ - Unix/Nested_Environment.thy Unix/Unix.thy Unix/document/root.bib \ - Unix/document/root.tex - @$(ISABELLE_TOOL) usedir -m no_brackets -m no_type_brackets $(OUT)/HOL Unix - - -## HOL-ZF - -HOL-ZF: HOL $(LOG)/HOL-ZF.gz - -$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/LProd.thy \ - ZF/HOLZF.thy ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex - @$(ISABELLE_TOOL) usedir $(OUT)/HOL ZF - - -## HOL-Imperative_HOL - -HOL-Imperative_HOL: HOL $(LOG)/HOL-Imperative_HOL.gz - -$(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL \ - Library/Code_Integer.thy \ - Library/Code_Nat.thy \ - Library/Code_Natural.thy \ - Library/Efficient_Nat.thy \ - Imperative_HOL/Array.thy \ - Imperative_HOL/Heap.thy \ - Imperative_HOL/Heap_Monad.thy \ - Imperative_HOL/Imperative_HOL.thy \ - Imperative_HOL/Imperative_HOL_ex.thy \ - Imperative_HOL/Mrec.thy \ - Imperative_HOL/Ref.thy \ - Imperative_HOL/ROOT.ML \ - Imperative_HOL/ex/Imperative_Quicksort.thy \ - Imperative_HOL/ex/Imperative_Reverse.thy \ - Imperative_HOL/ex/Linked_Lists.thy \ - Imperative_HOL/ex/SatChecker.thy \ - Imperative_HOL/ex/Sorted_List.thy \ - Imperative_HOL/ex/Subarray.thy \ - Imperative_HOL/ex/Sublist.thy - @$(ISABELLE_TOOL) usedir -g true -m iff -m no_brackets $(OUT)/HOL Imperative_HOL - - -## HOL-Decision_Procs - -HOL-Decision_Procs: HOL $(LOG)/HOL-Decision_Procs.gz - -$(LOG)/HOL-Decision_Procs.gz: $(OUT)/HOL \ - Library/Code_Integer.thy \ - Library/Code_Nat.thy \ - Library/Code_Natural.thy \ - Library/Efficient_Nat.thy \ - Decision_Procs/Approximation.thy \ - Decision_Procs/Commutative_Ring.thy \ - Decision_Procs/Commutative_Ring_Complete.thy \ - Decision_Procs/Cooper.thy \ - Decision_Procs/Decision_Procs.thy \ - Decision_Procs/Dense_Linear_Order.thy \ - Decision_Procs/Ferrack.thy \ - Decision_Procs/MIR.thy \ - Decision_Procs/Parametric_Ferrante_Rackoff.thy \ - Decision_Procs/Polynomial_List.thy \ - Decision_Procs/ROOT.ML \ - Decision_Procs/Reflected_Multivariate_Polynomial.thy \ - Decision_Procs/commutative_ring_tac.ML \ - Decision_Procs/cooper_tac.ML \ - Decision_Procs/ex/Approximation_Ex.thy \ - Decision_Procs/ex/Commutative_Ring_Ex.thy \ - Decision_Procs/ex/Dense_Linear_Order_Ex.thy \ - Decision_Procs/ferrack_tac.ML \ - Decision_Procs/ferrante_rackoff.ML \ - Decision_Procs/ferrante_rackoff_data.ML \ - Decision_Procs/langford.ML \ - Decision_Procs/langford_data.ML \ - Decision_Procs/mir_tac.ML - @$(ISABELLE_TOOL) usedir $(OUT)/HOL Decision_Procs - - -## HOL-Proofs - -HOL-Proofs: Pure $(OUT)/HOL-Proofs - -$(OUT)/HOL-Proofs: main.ML $(MAIN_DEPENDENCIES) - @$(ISABELLE_TOOL) usedir -b -f main.ML -g true -p 2 -q 0 $(OUT)/Pure HOL-Proofs - - -## HOL-Proofs-ex - -HOL-Proofs-ex: HOL-Proofs $(LOG)/HOL-Proofs-ex.gz - -$(LOG)/HOL-Proofs-ex.gz: $(OUT)/HOL-Proofs \ - Proofs/ex/ROOT.ML Proofs/ex/Hilbert_Classical.thy - @cd Proofs; $(ISABELLE_TOOL) usedir -p 2 -q 0 $(OUT)/HOL-Proofs ex - - -## HOL-Proofs-Extraction - -HOL-Proofs-Extraction: HOL-Proofs $(LOG)/HOL-Proofs-Extraction.gz - -$(LOG)/HOL-Proofs-Extraction.gz: $(OUT)/HOL-Proofs \ - Library/Code_Integer.thy Library/Code_Nat.thy \ - Library/Code_Natural.thy Library/Efficient_Nat.thy \ - Proofs/Extraction/Euclid.thy \ - Proofs/Extraction/Greatest_Common_Divisor.thy \ - Proofs/Extraction/Higman.thy \ - Proofs/Extraction/Higman_Extraction.thy \ - Proofs/Extraction/Pigeonhole.thy \ - Proofs/Extraction/QuotRem.thy Proofs/Extraction/ROOT.ML \ - Proofs/Extraction/Util.thy Proofs/Extraction/Warshall.thy \ - Proofs/Extraction/document/root.tex \ - Proofs/Extraction/document/root.bib - @cd Proofs; $(ISABELLE_TOOL) usedir -p 2 -q 0 $(OUT)/HOL-Proofs Extraction - - -## HOL-Proofs-Lambda - -HOL-Proofs-Lambda: HOL-Proofs $(LOG)/HOL-Proofs-Lambda.gz - -$(LOG)/HOL-Proofs-Lambda.gz: $(OUT)/HOL-Proofs \ - Proofs/Lambda/Commutation.thy Proofs/Lambda/Eta.thy \ - Proofs/Lambda/InductTermi.thy Proofs/Lambda/Lambda.thy \ - Proofs/Lambda/ListApplication.thy Proofs/Lambda/ListBeta.thy \ - Proofs/Lambda/ListOrder.thy Proofs/Lambda/NormalForm.thy \ - Proofs/Lambda/ParRed.thy Proofs/Lambda/Standardization.thy \ - Proofs/Lambda/StrongNorm.thy Proofs/Lambda/Type.thy \ - Proofs/Lambda/WeakNorm.thy Proofs/Lambda/ROOT.ML \ - Proofs/Lambda/document/root.bib Proofs/Lambda/document/root.tex - @cd Proofs; $(ISABELLE_TOOL) usedir -g true -m no_brackets -p 2 -q 0 $(OUT)/HOL-Proofs Lambda - - -## HOL-Prolog - -HOL-Prolog: HOL $(LOG)/HOL-Prolog.gz - -$(LOG)/HOL-Prolog.gz: $(OUT)/HOL Prolog/ROOT.ML Prolog/prolog.ML \ - Prolog/HOHH.thy Prolog/Test.thy Prolog/Func.thy Prolog/Type.thy - @$(ISABELLE_TOOL) usedir $(OUT)/HOL Prolog - - -## HOL-MicroJava - -HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz - -$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL MicroJava/ROOT.ML \ - MicroJava/Comp/AuxLemmas.thy MicroJava/Comp/CorrComp.thy \ - MicroJava/Comp/CorrCompTp.thy MicroJava/Comp/DefsComp.thy \ - MicroJava/Comp/Index.thy MicroJava/Comp/LemmasComp.thy \ - MicroJava/Comp/TranslComp.thy MicroJava/Comp/TranslCompTp.thy \ - MicroJava/Comp/TypeInf.thy MicroJava/J/Conform.thy \ - MicroJava/J/Eval.thy MicroJava/J/JBasis.thy \ - MicroJava/J/JTypeSafe.thy MicroJava/J/Decl.thy MicroJava/J/State.thy \ - MicroJava/J/Term.thy MicroJava/J/Type.thy MicroJava/J/TypeRel.thy \ - MicroJava/J/WellForm.thy MicroJava/J/Value.thy \ - MicroJava/J/WellType.thy MicroJava/J/Example.thy \ - MicroJava/J/JListExample.thy MicroJava/JVM/JVMExec.thy \ - MicroJava/JVM/JVMInstructions.thy MicroJava/JVM/JVMState.thy \ - MicroJava/JVM/JVMExecInstr.thy MicroJava/JVM/JVMListExample.thy \ - MicroJava/JVM/JVMExceptions.thy MicroJava/DFA/Abstract_BV.thy \ - MicroJava/DFA/Err.thy MicroJava/DFA/Kildall.thy \ - MicroJava/DFA/LBVComplete.thy MicroJava/DFA/LBVCorrect.thy \ - MicroJava/DFA/LBVSpec.thy MicroJava/DFA/Listn.thy \ - MicroJava/DFA/Opt.thy MicroJava/DFA/Product.thy \ - MicroJava/DFA/SemilatAlg.thy MicroJava/DFA/Semilat.thy \ - MicroJava/DFA/Semilattices.thy \ - MicroJava/DFA/Typing_Framework_err.thy \ - MicroJava/DFA/Typing_Framework.thy MicroJava/BV/BVSpec.thy \ - MicroJava/BV/BVSpecTypeSafe.thy MicroJava/BV/Correct.thy \ - MicroJava/BV/JType.thy MicroJava/BV/JVM.thy MicroJava/BV/JVMType.thy \ - MicroJava/BV/Effect.thy MicroJava/BV/EffectMono.thy \ - MicroJava/BV/Typing_Framework_JVM.thy MicroJava/BV/BVExample.thy \ - MicroJava/BV/LBVJVM.thy MicroJava/document/root.bib \ - MicroJava/document/root.tex MicroJava/document/introduction.tex - @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL MicroJava - - -## HOL-NanoJava - -HOL-NanoJava: HOL $(LOG)/HOL-NanoJava.gz - -$(LOG)/HOL-NanoJava.gz: $(OUT)/HOL NanoJava/ROOT.ML NanoJava/Term.thy \ - NanoJava/Decl.thy NanoJava/TypeRel.thy NanoJava/State.thy \ - NanoJava/OpSem.thy NanoJava/AxSem.thy NanoJava/AxSem.thy \ - NanoJava/document/root.bib NanoJava/document/root.tex - @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NanoJava - - -## HOL-Bali - -HOL-Bali: HOL $(LOG)/HOL-Bali.gz - -$(LOG)/HOL-Bali.gz: $(OUT)/HOL Bali/AxCompl.thy Bali/AxExample.thy \ - Bali/AxSem.thy Bali/AxSound.thy Bali/Basis.thy Bali/Conform.thy \ - Bali/Decl.thy Bali/DeclConcepts.thy Bali/Eval.thy Bali/Evaln.thy \ - Bali/Example.thy Bali/Name.thy Bali/ROOT.ML Bali/State.thy \ - Bali/Table.thy Bali/Term.thy Bali/Trans.thy Bali/Type.thy \ - Bali/TypeRel.thy Bali/TypeSafe.thy Bali/Value.thy Bali/WellForm.thy \ - Bali/DefiniteAssignment.thy Bali/DefiniteAssignmentCorrect.thy \ - Bali/WellType.thy Bali/document/root.tex - @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Bali - - -## HOL-IOA - -HOL-IOA: HOL $(LOG)/HOL-IOA.gz +HOL-IMP: + @$(ISABELLE_TOOL) build -b HOL-IMP -$(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.thy IOA/IOA.thy IOA/ROOT.ML \ - IOA/Solve.thy - @$(ISABELLE_TOOL) usedir $(OUT)/HOL IOA - - -## HOL-Lattice - -HOL-Lattice: HOL $(LOG)/HOL-Lattice.gz - -$(LOG)/HOL-Lattice.gz: $(OUT)/HOL Lattice/Bounds.thy \ - Lattice/CompleteLattice.thy Lattice/Lattice.thy Lattice/Orders.thy \ - Lattice/ROOT.ML Lattice/document/root.tex - @$(ISABELLE_TOOL) usedir $(OUT)/HOL Lattice - - -## HOL-ex - -HOL-ex: HOL $(LOG)/HOL-ex.gz - -$(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy \ - Library/Code_Integer.thy Library/Code_Nat.thy \ - Library/Code_Natural.thy Library/Efficient_Nat.thy \ - Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy \ - ex/Arith_Examples.thy ex/BT.thy \ - ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradox.thy ex/CTL.thy \ - ex/Case_Product.thy ex/Chinese.thy ex/Classical.thy \ - ex/Code_Nat_examples.thy \ - ex/Coercion_Examples.thy ex/Coherent.thy ex/Dedekind_Real.thy \ - ex/Eval_Examples.thy ex/Executable_Relation.thy \ - ex/FinFunPred.thy ex/Fundefs.thy \ - ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy \ - ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy \ - ex/Higher_Order_Logic.thy ex/Iff_Oracle.thy ex/Induction_Schema.thy \ - ex/Interpretation_with_Defs.thy ex/Intuitionistic.thy \ - ex/Lagrange.thy ex/List_to_Set_Comprehension_Examples.thy \ - ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy ex/Meson_Test.thy \ - ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy \ - ex/Normalization_by_Evaluation.thy ex/Numeral_Representation.thy \ - ex/Parallel_Example.thy \ - ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \ - ex/Quicksort.thy ex/ROOT.ML \ - ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy \ - ex/SAT_Examples.thy ex/Serbian.thy \ - ex/Set_Comprehension_Pointfree_Tests.thy ex/Set_Theory.thy \ - ex/Simproc_Tests.thy ex/SVC_Oracle.thy \ - ex/Seq.thy ex/Sqrt.thy ex/Sqrt_Script.thy \ - ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy \ - ex/Transfer_Int_Nat.thy \ - ex/Tree23.thy ex/Unification.thy ex/While_Combinator_Example.thy \ - ex/document/root.bib ex/document/root.tex ex/svc_funcs.ML \ - ex/svc_test.thy ../Tools/interpretation_with_defs.ML - @$(ISABELLE_TOOL) usedir $(OUT)/HOL ex - - -## HOL-Isar_Examples - -HOL-Isar_Examples: HOL $(LOG)/HOL-Isar_Examples.gz - -$(LOG)/HOL-Isar_Examples.gz: $(OUT)/HOL Isar_Examples/Basic_Logic.thy \ - Isar_Examples/Cantor.thy Isar_Examples/Drinker.thy \ - Isar_Examples/Expr_Compiler.thy Isar_Examples/Fibonacci.thy \ - Isar_Examples/Group.thy Isar_Examples/Group_Context.thy \ - Isar_Examples/Group_Notepad.thy Isar_Examples/Hoare.thy \ - Isar_Examples/Hoare_Ex.thy Isar_Examples/Knaster_Tarski.thy \ - Isar_Examples/Mutilated_Checkerboard.thy \ - Isar_Examples/Nested_Datatype.thy Isar_Examples/Peirce.thy \ - Isar_Examples/Puzzle.thy Isar_Examples/Summation.thy \ - Isar_Examples/ROOT.ML Isar_Examples/document/proof.sty \ - Isar_Examples/document/root.bib Isar_Examples/document/root.tex \ - Isar_Examples/document/style.tex Hoare/hoare_tac.ML \ - Number_Theory/Primes.thy - @$(ISABELLE_TOOL) usedir $(OUT)/HOL Isar_Examples - - -## HOL-SET_Protocol - -HOL-SET_Protocol: HOL $(LOG)/HOL-SET_Protocol.gz - -$(LOG)/HOL-SET_Protocol.gz: $(OUT)/HOL SET_Protocol/ROOT.ML \ - SET_Protocol/Message_SET.thy SET_Protocol/Event_SET.thy \ - SET_Protocol/Public_SET.thy SET_Protocol/Cardholder_Registration.thy \ - SET_Protocol/Merchant_Registration.thy SET_Protocol/Purchase.thy \ - SET_Protocol/SET_Protocol.thy SET_Protocol/document/root.tex - @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL SET_Protocol - - -## HOL-Matrix_LP - -HOL-Matrix_LP: HOL $(LOG)/HOL-Matrix_LP.gz - -$(LOG)/HOL-Matrix_LP.gz: $(OUT)/HOL Matrix_LP/ComputeFloat.thy \ - Matrix_LP/ComputeHOL.thy Matrix_LP/ComputeNumeral.thy \ - Matrix_LP/Compute_Oracle/Compute_Oracle.thy \ - Matrix_LP/Compute_Oracle/am.ML \ - Matrix_LP/Compute_Oracle/am_compiler.ML \ - Matrix_LP/Compute_Oracle/am_ghc.ML \ - Matrix_LP/Compute_Oracle/am_interpreter.ML \ - Matrix_LP/Compute_Oracle/am_sml.ML \ - Matrix_LP/Compute_Oracle/compute.ML \ - Matrix_LP/Compute_Oracle/linker.ML Matrix_LP/Cplex.thy \ - Matrix_LP/CplexMatrixConverter.ML Matrix_LP/Cplex_tools.ML \ - Matrix_LP/FloatSparseMatrixBuilder.ML Matrix_LP/LP.thy \ - Matrix_LP/Matrix.thy Matrix_LP/ROOT.ML Matrix_LP/SparseMatrix.thy \ - Matrix_LP/document/root.tex Matrix_LP/fspmlp.ML \ - Matrix_LP/matrixlp.ML Tools/float_arith.ML - @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Matrix_LP - - -## TLA - -TLA: HOL $(OUT)/TLA - -$(OUT)/TLA: $(OUT)/HOL TLA/Action.thy TLA/Init.thy TLA/Intensional.thy \ - TLA/ROOT.ML TLA/Stfun.thy TLA/TLA.thy - @cd TLA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL TLA - - -## TLA-Inc - -TLA-Inc: TLA $(LOG)/TLA-Inc.gz - -$(LOG)/TLA-Inc.gz: $(OUT)/TLA TLA/Inc/Inc.thy - @cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Inc - - -## TLA-Buffer - -TLA-Buffer: TLA $(LOG)/TLA-Buffer.gz - -$(LOG)/TLA-Buffer.gz: $(OUT)/TLA TLA/Buffer/Buffer.thy \ - TLA/Buffer/DBuffer.thy - @cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Buffer - - -## TLA-Memory - -TLA-Memory: TLA $(LOG)/TLA-Memory.gz - -$(LOG)/TLA-Memory.gz: $(OUT)/TLA TLA/Memory/MemClerk.thy \ - TLA/Memory/MemClerkParameters.thy TLA/Memory/Memory.thy \ - TLA/Memory/MemoryImplementation.thy TLA/Memory/MemoryParameters.thy \ - TLA/Memory/ProcedureInterface.thy TLA/Memory/RPC.thy \ - TLA/Memory/RPCMemoryParams.thy TLA/Memory/RPCParameters.thy - @cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Memory - - -## HOL-TPTP - -HOL-TPTP: HOL $(LOG)/HOL-TPTP.gz - -$(LOG)/HOL-TPTP.gz: $(OUT)/HOL \ - TPTP/ATP_Problem_Import.thy \ - TPTP/ATP_Theory_Export.thy \ - TPTP/MaSh_Eval.thy \ - TPTP/MaSh_Export.thy \ - TPTP/ROOT.ML \ - TPTP/THF_Arith.thy \ - TPTP/TPTP_Parser.thy \ - TPTP/TPTP_Parser/ml_yacc_lib.ML \ - TPTP/TPTP_Parser/tptp_interpret.ML \ - TPTP/TPTP_Parser/tptp_lexyacc.ML \ - TPTP/TPTP_Parser/tptp_parser.ML \ - TPTP/TPTP_Parser/tptp_problem_name.ML \ - TPTP/TPTP_Parser/tptp_syntax.ML \ - TPTP/TPTP_Parser_Test.thy \ - TPTP/atp_problem_import.ML \ - TPTP/atp_theory_export.ML \ - TPTP/mash_eval.ML \ - TPTP/mash_export.ML \ - TPTP/sledgehammer_tactics.ML - @$(ISABELLE_TOOL) usedir $(OUT)/HOL TPTP - - -## HOL-Multivariate_Analysis - -HOL-Multivariate_Analysis: HOL $(OUT)/HOL-Multivariate_Analysis +HOL-Multivariate_Analysis: + @$(ISABELLE_TOOL) build -b HOL-Multivariate_Analysis -$(OUT)/HOL-Multivariate_Analysis: $(OUT)/HOL \ - Multivariate_Analysis/Brouwer_Fixpoint.thy \ - Multivariate_Analysis/Cartesian_Euclidean_Space.thy \ - Multivariate_Analysis/Convex_Euclidean_Space.thy \ - Multivariate_Analysis/Derivative.thy \ - Multivariate_Analysis/Determinants.thy \ - Multivariate_Analysis/Euclidean_Space.thy \ - Multivariate_Analysis/Extended_Real_Limits.thy \ - Multivariate_Analysis/Fashoda.thy \ - Multivariate_Analysis/Finite_Cartesian_Product.thy \ - Multivariate_Analysis/Integration.certs \ - Multivariate_Analysis/Integration.thy \ - Multivariate_Analysis/L2_Norm.thy \ - Multivariate_Analysis/Linear_Algebra.thy \ - Multivariate_Analysis/Multivariate_Analysis.thy \ - Multivariate_Analysis/Norm_Arith.thy \ - Multivariate_Analysis/Operator_Norm.thy \ - Multivariate_Analysis/Path_Connected.thy \ - Multivariate_Analysis/ROOT.ML \ - Multivariate_Analysis/Real_Integration.thy \ - Multivariate_Analysis/Topology_Euclidean_Space.thy \ - Multivariate_Analysis/document/root.tex \ - Multivariate_Analysis/normarith.ML Library/Glbs.thy \ - Library/Extended_Real.thy Library/Indicator_Function.thy \ - Library/Inner_Product.thy Library/Numeral_Type.thy Library/Convex.thy \ - Library/FrechetDeriv.thy Library/Product_Vector.thy \ - Library/Product_plus.thy Library/Sum_of_Squares.thy - @cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Multivariate_Analysis - - -## HOL-Probability - -HOL-Probability: HOL-Multivariate_Analysis $(OUT)/HOL-Probability - -$(OUT)/HOL-Probability: $(OUT)/HOL-Multivariate_Analysis \ - Probability/Binary_Product_Measure.thy Probability/Borel_Space.thy \ - Probability/Caratheodory.thy Probability/Complete_Measure.thy \ - Probability/ex/Dining_Cryptographers.thy \ - Probability/ex/Koepf_Duermuth_Countermeasure.thy \ - Probability/Finite_Product_Measure.thy \ - Probability/Independent_Family.thy \ - Probability/Infinite_Product_Measure.thy Probability/Information.thy \ - Probability/Lebesgue_Integration.thy Probability/Lebesgue_Measure.thy \ - Probability/Measure_Space.thy Probability/Probability_Measure.thy \ - Probability/Probability.thy Probability/Radon_Nikodym.thy \ - Probability/ROOT.ML Probability/Sigma_Algebra.thy \ - Library/Countable.thy Library/FuncSet.thy Library/Nat_Bijection.thy - @cd Probability; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Multivariate_Analysis HOL-Probability - - -## HOL-Nominal - -HOL-Nominal: HOL $(OUT)/HOL-Nominal - -$(OUT)/HOL-Nominal: $(OUT)/HOL Nominal/ROOT.ML \ - Nominal/Nominal.thy \ - Nominal/nominal_atoms.ML \ - Nominal/nominal_datatype.ML \ - Nominal/nominal_fresh_fun.ML \ - Nominal/nominal_induct.ML \ - Nominal/nominal_inductive.ML \ - Nominal/nominal_inductive2.ML \ - Nominal/nominal_permeq.ML \ - Nominal/nominal_primrec.ML \ - Nominal/nominal_thmdecls.ML \ - Library/Infinite_Set.thy - @cd Nominal; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Nominal - - -## HOL-Nominal-Examples - -HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz - -$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal \ - Nominal/Examples/Nominal_Examples.thy \ - Nominal/Examples/CK_Machine.thy \ - Nominal/Examples/CR.thy \ - Nominal/Examples/CR_Takahashi.thy \ - Nominal/Examples/Class1.thy \ - Nominal/Examples/Class2.thy \ - Nominal/Examples/Class3.thy \ - Nominal/Examples/Compile.thy \ - Nominal/Examples/Contexts.thy \ - Nominal/Examples/Crary.thy \ - Nominal/Examples/Fsub.thy \ - Nominal/Examples/Height.thy \ - Nominal/Examples/Lam_Funs.thy \ - Nominal/Examples/Lambda_mu.thy \ - Nominal/Examples/LocalWeakening.thy \ - Nominal/Examples/Pattern.thy \ - Nominal/Examples/ROOT.ML \ - Nominal/Examples/SN.thy \ - Nominal/Examples/SOS.thy \ - Nominal/Examples/Standardization.thy \ - Nominal/Examples/Support.thy \ - Nominal/Examples/Type_Preservation.thy \ - Nominal/Examples/VC_Condition.thy \ - Nominal/Examples/W.thy \ - Nominal/Examples/Weakening.thy - @cd Nominal; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Nominal Examples - - -## HOL-Word - -HOL-Word: HOL $(OUT)/HOL-Word - -$(OUT)/HOL-Word: $(OUT)/HOL Word/ROOT.ML Library/Boolean_Algebra.thy \ - Library/Numeral_Type.thy Word/Misc_Numeric.thy Word/Misc_Typedef.thy \ - Word/Type_Length.thy Word/Bit_Representation.thy Word/Bit_Int.thy \ - Word/Bool_List_Representation.thy Word/Bit_Operations.thy \ - Word/Word.thy Word/WordBitwise.thy Word/document/root.tex \ - Word/document/root.bib Word/Tools/smt_word.ML Word/Tools/word_lib.ML - @cd Word; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Word - - -## HOL-Word-Examples - -HOL-Word-Examples: HOL-Word $(LOG)/HOL-Word-Examples.gz - -$(LOG)/HOL-Word-Examples.gz: $(OUT)/HOL-Word Word/Examples/ROOT.ML \ - Word/Examples/WordExamples.thy - @cd Word; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Word Examples - - -## HOL-Statespace - -HOL-Statespace: HOL $(LOG)/HOL-Statespace.gz - -$(LOG)/HOL-Statespace.gz: $(OUT)/HOL Statespace/ROOT.ML \ - Statespace/DistinctTreeProver.thy Statespace/StateFun.thy \ - Statespace/StateSpaceLocale.thy Statespace/StateSpaceSyntax.thy \ - Statespace/StateSpaceEx.thy Statespace/distinct_tree_prover.ML \ - Statespace/state_space.ML Statespace/state_fun.ML \ - Statespace/document/root.tex - @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Statespace - - -## HOL-NSA - -HOL-NSA: HOL $(OUT)/HOL-NSA - -$(OUT)/HOL-NSA: $(OUT)/HOL NSA/CLim.thy NSA/CStar.thy NSA/NSCA.thy \ - NSA/NSComplex.thy NSA/HDeriv.thy NSA/HLim.thy NSA/HLog.thy \ - NSA/HSEQ.thy NSA/HSeries.thy NSA/HTranscendental.thy \ - NSA/Hypercomplex.thy NSA/HyperDef.thy NSA/HyperNat.thy \ - NSA/Hyperreal.thy NSA/Filter.thy NSA/NatStar.thy NSA/NSA.thy \ - NSA/StarDef.thy NSA/Star.thy NSA/transfer.ML \ - Library/Infinite_Set.thy Library/Zorn.thy NSA/ROOT.ML - @cd NSA; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-NSA - - -## HOL-NSA-Examples - -HOL-NSA-Examples: HOL-NSA $(LOG)/HOL-NSA-Examples.gz - -$(LOG)/HOL-NSA-Examples.gz: $(OUT)/HOL-NSA NSA/Examples/ROOT.ML \ - NSA/Examples/NSPrimes.thy - @cd NSA; $(ISABELLE_TOOL) usedir $(OUT)/HOL-NSA Examples - - -## HOL-Mirabelle - -HOL-Mirabelle: HOL $(LOG)/HOL-Mirabelle.gz - -$(LOG)/HOL-Mirabelle.gz: $(OUT)/HOL Mirabelle/Mirabelle_Test.thy \ - Mirabelle/Mirabelle.thy Mirabelle/Tools/mirabelle.ML \ - Mirabelle/ROOT.ML Mirabelle/Tools/mirabelle_arith.ML \ - Mirabelle/Tools/mirabelle_metis.ML \ - Mirabelle/Tools/mirabelle_quickcheck.ML \ - Mirabelle/Tools/mirabelle_refute.ML \ - Mirabelle/Tools/mirabelle_sledgehammer.ML \ - Mirabelle/Tools/mirabelle_sledgehammer_filter.ML \ - Mirabelle/Tools/mirabelle_try0.ML \ - TPTP/sledgehammer_tactics.ML Mirabelle/lib/Tools/mirabelle \ - Mirabelle/lib/scripts/mirabelle.pl Library/FrechetDeriv.thy \ - Library/Inner_Product.thy - @$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle - @cd Library; $(ISABELLE_TOOL) mirabelle -q arith Inner_Product.thy # some arbitrary small test case - - -## HOL-Word-SMT_Examples - -HOL-Word-SMT_Examples: HOL-Word $(LOG)/HOL-Word-SMT_Examples.gz - -$(LOG)/HOL-Word-SMT_Examples.gz: $(OUT)/HOL-Word SMT_Examples/ROOT.ML \ - SMT_Examples/SMT_Examples.thy SMT_Examples/SMT_Examples.certs \ - SMT_Examples/SMT_Word_Examples.thy SMT_Examples/SMT_Tests.thy \ - SMT_Examples/SMT_Word_Examples.certs SMT_Examples/SMT_Tests.certs - @$(ISABELLE_TOOL) usedir $(OUT)/HOL-Word SMT_Examples - - -## HOL-Boogie - -HOL-Boogie: HOL-Word $(OUT)/HOL-Boogie - -$(OUT)/HOL-Boogie: $(OUT)/HOL-Word Boogie/ROOT.ML Boogie/Boogie.thy \ - Boogie/Tools/boogie_vcs.ML Boogie/Tools/boogie_loader.ML \ - Boogie/Tools/boogie_commands.ML Boogie/Tools/boogie_tactics.ML - @cd Boogie; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-Boogie - - -## HOL-Boogie_Examples - -HOL-Boogie-Examples: HOL-Boogie $(LOG)/HOL-Boogie-Examples.gz - -$(LOG)/HOL-Boogie-Examples.gz: $(OUT)/HOL-Boogie \ - Boogie/Examples/ROOT.ML Boogie/Examples/Boogie_Max.thy \ - Boogie/Examples/Boogie_Max.b2i Boogie/Examples/Boogie_Dijkstra.thy \ - Boogie/Examples/VCC_Max.thy Boogie/Examples/Boogie_Dijkstra.b2i \ - Boogie/Examples/VCC_Max.b2i Boogie/Examples/Boogie_Max.certs \ - Boogie/Examples/Boogie_Dijkstra.certs Boogie/Examples/VCC_Max.certs - @cd Boogie; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Boogie Examples - - -## HOL-SPARK - -HOL-SPARK: HOL-Word $(OUT)/HOL-SPARK - -$(OUT)/HOL-SPARK: $(OUT)/HOL-Word SPARK/ROOT.ML \ - SPARK/SPARK.thy SPARK/SPARK_Setup.thy \ - SPARK/Tools/fdl_lexer.ML SPARK/Tools/fdl_parser.ML \ - SPARK/Tools/spark_commands.ML SPARK/Tools/spark_vcs.ML - @cd SPARK; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SPARK - - -## HOL-SPARK-Examples - -HOL-SPARK-Examples: HOL-SPARK $(LOG)/HOL-SPARK-Examples.gz +HOL-Nominal: + @$(ISABELLE_TOOL) build -b HOL-Nominal -$(LOG)/HOL-SPARK-Examples.gz: $(OUT)/HOL-SPARK \ - SPARK/Examples/ROOT.ML \ - SPARK/Examples/Gcd/Greatest_Common_Divisor.thy \ - SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.fdl \ - SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.rls \ - SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.siv \ - SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy \ - SPARK/Examples/Liseq/liseq/liseq_length.fdl \ - SPARK/Examples/Liseq/liseq/liseq_length.rls \ - SPARK/Examples/Liseq/liseq/liseq_length.siv \ - SPARK/Examples/RIPEMD-160/F.thy SPARK/Examples/RIPEMD-160/Hash.thy \ - SPARK/Examples/RIPEMD-160/K_L.thy SPARK/Examples/RIPEMD-160/K_R.thy \ - SPARK/Examples/RIPEMD-160/R_L.thy \ - SPARK/Examples/RIPEMD-160/RMD_Lemmas.thy \ - SPARK/Examples/RIPEMD-160/RMD_Specification.thy \ - SPARK/Examples/RIPEMD-160/RMD.thy SPARK/Examples/RIPEMD-160/Round.thy \ - SPARK/Examples/RIPEMD-160/R_R.thy SPARK/Examples/RIPEMD-160/S_L.thy \ - SPARK/Examples/RIPEMD-160/S_R.thy \ - SPARK/Examples/RIPEMD-160/rmd/f.fdl \ - SPARK/Examples/RIPEMD-160/rmd/f.rls \ - SPARK/Examples/RIPEMD-160/rmd/f.siv \ - SPARK/Examples/RIPEMD-160/rmd/hash.fdl \ - SPARK/Examples/RIPEMD-160/rmd/hash.rls \ - SPARK/Examples/RIPEMD-160/rmd/hash.siv \ - SPARK/Examples/RIPEMD-160/rmd/k_l.fdl \ - SPARK/Examples/RIPEMD-160/rmd/k_l.rls \ - SPARK/Examples/RIPEMD-160/rmd/k_l.siv \ - SPARK/Examples/RIPEMD-160/rmd/k_r.fdl \ - SPARK/Examples/RIPEMD-160/rmd/k_r.rls \ - SPARK/Examples/RIPEMD-160/rmd/k_r.siv \ - SPARK/Examples/RIPEMD-160/rmd/r_l.fdl \ - SPARK/Examples/RIPEMD-160/rmd/r_l.rls \ - SPARK/Examples/RIPEMD-160/rmd/r_l.siv \ - SPARK/Examples/RIPEMD-160/rmd/round.fdl \ - SPARK/Examples/RIPEMD-160/rmd/round.rls \ - SPARK/Examples/RIPEMD-160/rmd/round.siv \ - SPARK/Examples/RIPEMD-160/rmd/r_r.fdl \ - SPARK/Examples/RIPEMD-160/rmd/r_r.rls \ - SPARK/Examples/RIPEMD-160/rmd/r_r.siv \ - SPARK/Examples/RIPEMD-160/rmd/s_l.fdl \ - SPARK/Examples/RIPEMD-160/rmd/s_l.rls \ - SPARK/Examples/RIPEMD-160/rmd/s_l.siv \ - SPARK/Examples/RIPEMD-160/rmd/s_r.fdl \ - SPARK/Examples/RIPEMD-160/rmd/s_r.rls \ - SPARK/Examples/RIPEMD-160/rmd/s_r.siv - @cd SPARK; $(ISABELLE_TOOL) usedir $(OUT)/HOL-SPARK Examples - - -## HOL-SPARK-Manual - -HOL-SPARK-Manual: HOL-SPARK $(LOG)/HOL-SPARK-Manual.gz - -$(LOG)/HOL-SPARK-Manual.gz: $(OUT)/HOL-SPARK \ - SPARK/Manual/ROOT.ML \ - SPARK/Manual/Complex_Types.thy \ - SPARK/Manual/Example_Verification.thy \ - SPARK/Manual/Proc1.thy \ - SPARK/Manual/Proc2.thy \ - SPARK/Manual/Reference.thy \ - SPARK/Manual/Simple_Greatest_Common_Divisor.thy \ - SPARK/Manual/VC_Principles.thy \ - SPARK/Manual/complex_types_app/initialize.fdl \ - SPARK/Manual/complex_types_app/initialize.rls \ - SPARK/Manual/complex_types_app/initialize.siv \ - SPARK/Manual/loop_invariant/proc1.fdl \ - SPARK/Manual/loop_invariant/proc1.rls \ - SPARK/Manual/loop_invariant/proc1.siv \ - SPARK/Manual/loop_invariant/proc2.fdl \ - SPARK/Manual/loop_invariant/proc2.rls \ - SPARK/Manual/loop_invariant/proc2.siv \ - SPARK/Manual/simple_greatest_common_divisor/g_c_d.fdl \ - SPARK/Manual/simple_greatest_common_divisor/g_c_d.rls \ - SPARK/Manual/simple_greatest_common_divisor/g_c_d.siv \ - SPARK/Manual/document/complex_types.ads \ - SPARK/Manual/document/complex_types_app.adb \ - SPARK/Manual/document/complex_types_app.ads \ - SPARK/Manual/document/loop_invariant.adb \ - SPARK/Manual/document/loop_invariant.ads \ - SPARK/Manual/document/Simple_Gcd.adb \ - SPARK/Manual/document/Simple_Gcd.ads \ - SPARK/Manual/document/intro.tex \ - SPARK/Manual/document/root.tex \ - SPARK/Manual/document/root.bib \ - SPARK/Examples/Gcd/Greatest_Common_Divisor.thy \ - SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.fdl \ - SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.rls \ - SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.siv - @cd SPARK; $(ISABELLE_TOOL) usedir $(OUT)/HOL-SPARK Manual - - -## HOL-Mutabelle - -HOL-Mutabelle: HOL $(LOG)/HOL-Mutabelle.gz - -$(LOG)/HOL-Mutabelle.gz: $(OUT)/HOL Mutabelle/MutabelleExtra.thy \ - Mutabelle/ROOT.ML Mutabelle/mutabelle.ML \ - Mutabelle/mutabelle_extra.ML - @$(ISABELLE_TOOL) usedir $(OUT)/HOL Mutabelle - -## HOL-Quickcheck_Examples - -HOL-Quickcheck_Examples: HOL $(LOG)/HOL-Quickcheck_Examples.gz - -$(LOG)/HOL-Quickcheck_Examples.gz: $(OUT)/HOL \ - Quickcheck_Examples/ROOT.ML \ - Quickcheck_Examples/Completeness.thy \ - Quickcheck_Examples/Hotel_Example.thy \ - Quickcheck_Examples/Quickcheck_Examples.thy \ - Quickcheck_Examples/Quickcheck_Interfaces.thy \ - Quickcheck_Examples/Quickcheck_Lattice_Examples.thy \ - Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy - @$(ISABELLE_TOOL) usedir $(OUT)/HOL Quickcheck_Examples - -## HOL-Quotient_Examples - -HOL-Quotient_Examples: HOL $(LOG)/HOL-Quotient_Examples.gz - -$(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL \ - Quotient_Examples/DList.thy \ - Quotient_Examples/FSet.thy \ - Quotient_Examples/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy \ - Quotient_Examples/Lift_FSet.thy \ - Quotient_Examples/Lift_Set.thy \ - Quotient_Examples/Lift_Fun.thy Quotient_Examples/Lift_DList.thy - @$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples - - -## HOL-Predicate_Compile_Examples - -HOL-Predicate_Compile_Examples: HOL $(LOG)/HOL-Predicate_Compile_Examples.gz - -$(LOG)/HOL-Predicate_Compile_Examples.gz: $(OUT)/HOL \ - Predicate_Compile_Examples/ROOT.ML \ - Predicate_Compile_Examples/Predicate_Compile_Tests.thy \ - Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy \ - Predicate_Compile_Examples/Code_Prolog_Examples.thy \ - Predicate_Compile_Examples/Examples.thy \ - Predicate_Compile_Examples/Context_Free_Grammar_Example.thy \ - Predicate_Compile_Examples/Hotel_Example.thy \ - Predicate_Compile_Examples/Hotel_Example_Prolog.thy \ - Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy \ - Predicate_Compile_Examples/IMP_1.thy \ - Predicate_Compile_Examples/IMP_2.thy \ - Predicate_Compile_Examples/IMP_3.thy \ - Predicate_Compile_Examples/IMP_4.thy \ - Predicate_Compile_Examples/Lambda_Example.thy \ - Predicate_Compile_Examples/List_Examples.thy \ - Predicate_Compile_Examples/Reg_Exp_Example.thy - @$(ISABELLE_TOOL) usedir $(OUT)/HOL Predicate_Compile_Examples - - -## HOLCF - -HOLCF: HOL $(OUT)/HOLCF - -$(OUT)/HOLCF: $(OUT)/HOL \ - HOLCF/ROOT.ML \ - HOLCF/Adm.thy \ - HOLCF/Algebraic.thy \ - HOLCF/Bifinite.thy \ - HOLCF/Cfun.thy \ - HOLCF/Compact_Basis.thy \ - HOLCF/Completion.thy \ - HOLCF/Cont.thy \ - HOLCF/ConvexPD.thy \ - HOLCF/Cpodef.thy \ - HOLCF/Cprod.thy \ - HOLCF/Discrete.thy \ - HOLCF/Deflation.thy \ - HOLCF/Domain.thy \ - HOLCF/Domain_Aux.thy \ - HOLCF/Fixrec.thy \ - HOLCF/Fix.thy \ - HOLCF/Fun_Cpo.thy \ - HOLCF/HOLCF.thy \ - HOLCF/Lift.thy \ - HOLCF/LowerPD.thy \ - HOLCF/Map_Functions.thy \ - HOLCF/One.thy \ - HOLCF/Pcpo.thy \ - HOLCF/Plain_HOLCF.thy \ - HOLCF/Porder.thy \ - HOLCF/Powerdomains.thy \ - HOLCF/Product_Cpo.thy \ - HOLCF/Representable.thy \ - HOLCF/Sfun.thy \ - HOLCF/Sprod.thy \ - HOLCF/Ssum.thy \ - HOLCF/Tr.thy \ - HOLCF/Universal.thy \ - HOLCF/UpperPD.thy \ - HOLCF/Up.thy \ - HOLCF/Tools/cont_consts.ML \ - HOLCF/Tools/cont_proc.ML \ - HOLCF/Tools/holcf_library.ML \ - HOLCF/Tools/Domain/domain.ML \ - HOLCF/Tools/Domain/domain_axioms.ML \ - HOLCF/Tools/Domain/domain_constructors.ML \ - HOLCF/Tools/Domain/domain_induction.ML \ - HOLCF/Tools/Domain/domain_isomorphism.ML \ - HOLCF/Tools/Domain/domain_take_proofs.ML \ - HOLCF/Tools/cpodef.ML \ - HOLCF/Tools/domaindef.ML \ - HOLCF/Tools/fixrec.ML \ - HOLCF/document/root.tex - @cd HOLCF; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOLCF - - -## HOLCF-Tutorial - -HOLCF-Tutorial: HOLCF $(LOG)/HOLCF-Tutorial.gz - -$(LOG)/HOLCF-Tutorial.gz: $(OUT)/HOLCF \ - HOLCF/Tutorial/Domain_ex.thy \ - HOLCF/Tutorial/Fixrec_ex.thy \ - HOLCF/Tutorial/New_Domain.thy \ - HOLCF/Tutorial/document/root.tex \ - HOLCF/Tutorial/ROOT.ML - @cd HOLCF; $(ISABELLE_TOOL) usedir $(OUT)/HOLCF Tutorial - - -## HOLCF-Library - -HOLCF-Library: HOLCF $(LOG)/HOLCF-Library.gz +HOL-Word: + @$(ISABELLE_TOOL) build -b HOL-Word -$(LOG)/HOLCF-Library.gz: $(OUT)/HOLCF \ - Library/Extended_Nat.thy \ - HOLCF/Library/Defl_Bifinite.thy \ - HOLCF/Library/Bool_Discrete.thy \ - HOLCF/Library/Char_Discrete.thy \ - HOLCF/Library/HOL_Cpo.thy \ - HOLCF/Library/Int_Discrete.thy \ - HOLCF/Library/List_Cpo.thy \ - HOLCF/Library/List_Predomain.thy \ - HOLCF/Library/Nat_Discrete.thy \ - HOLCF/Library/Option_Cpo.thy \ - HOLCF/Library/Stream.thy \ - HOLCF/Library/Sum_Cpo.thy \ - HOLCF/Library/HOLCF_Library.thy \ - HOLCF/Library/ROOT.ML - @cd HOLCF; $(ISABELLE_TOOL) usedir $(OUT)/HOLCF Library - - -## HOLCF-IMP - -HOLCF-IMP: HOLCF $(LOG)/HOLCF-IMP.gz - -$(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF \ - HOLCF/IMP/HoareEx.thy \ - HOLCF/IMP/Denotational.thy \ - HOLCF/IMP/ROOT.ML \ - HOLCF/IMP/document/root.tex - @cd HOLCF; $(ISABELLE_TOOL) usedir $(OUT)/HOLCF IMP - - -## HOLCF-ex - -HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz - -$(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF \ - HOLCF/ex/Concurrency_Monad.thy \ - HOLCF/ex/Dagstuhl.thy \ - HOLCF/ex/Dnat.thy \ - HOLCF/ex/Domain_Proofs.thy \ - HOLCF/ex/Fix2.thy \ - HOLCF/ex/Focus_ex.thy \ - HOLCF/ex/Hoare.thy \ - HOLCF/ex/Letrec.thy \ - HOLCF/ex/Loop.thy \ - HOLCF/ex/Pattern_Match.thy \ - HOLCF/ex/Powerdomain_ex.thy \ - HOLCF/ex/ROOT.ML - @cd HOLCF; $(ISABELLE_TOOL) usedir $(OUT)/HOLCF ex - - -## HOLCF-FOCUS - -HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz - -$(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF HOLCF/FOCUS/ROOT.ML \ - Library/Extended_Nat.thy \ - HOLCF/Library/Stream.thy \ - HOLCF/FOCUS/Fstreams.thy \ - HOLCF/FOCUS/Fstream.thy \ - HOLCF/FOCUS/FOCUS.thy \ - HOLCF/FOCUS/Stream_adm.thy \ - HOLCF/FOCUS/Buffer.thy \ - HOLCF/FOCUS/Buffer_adm.thy \ - Library/Continuity.thy - @cd HOLCF; $(ISABELLE_TOOL) usedir $(OUT)/HOLCF FOCUS - - -## IOA - -IOA: HOLCF $(OUT)/IOA - -$(OUT)/IOA: $(OUT)/HOLCF \ - HOLCF/IOA/ROOT.ML \ - HOLCF/IOA/meta_theory/Traces.thy \ - HOLCF/IOA/meta_theory/Asig.thy \ - HOLCF/IOA/meta_theory/CompoScheds.thy \ - HOLCF/IOA/meta_theory/CompoTraces.thy \ - HOLCF/IOA/meta_theory/Seq.thy \ - HOLCF/IOA/meta_theory/RefCorrectness.thy \ - HOLCF/IOA/meta_theory/Automata.thy \ - HOLCF/IOA/meta_theory/ShortExecutions.thy \ - HOLCF/IOA/meta_theory/IOA.thy \ - HOLCF/IOA/meta_theory/Sequence.thy \ - HOLCF/IOA/meta_theory/CompoExecs.thy \ - HOLCF/IOA/meta_theory/RefMappings.thy \ - HOLCF/IOA/meta_theory/Compositionality.thy \ - HOLCF/IOA/meta_theory/TL.thy \ - HOLCF/IOA/meta_theory/TLS.thy \ - HOLCF/IOA/meta_theory/LiveIOA.thy \ - HOLCF/IOA/meta_theory/Pred.thy \ - HOLCF/IOA/meta_theory/Abstraction.thy \ - HOLCF/IOA/meta_theory/Simulations.thy \ - HOLCF/IOA/meta_theory/SimCorrectness.thy - @cd HOLCF/IOA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOLCF IOA - - -## IOA-ABP - -IOA-ABP: IOA $(LOG)/IOA-ABP.gz - -$(LOG)/IOA-ABP.gz: $(OUT)/IOA \ - HOLCF/IOA/ABP/Abschannel.thy \ - HOLCF/IOA/ABP/Abschannel_finite.thy \ - HOLCF/IOA/ABP/Action.thy \ - HOLCF/IOA/ABP/Check.ML \ - HOLCF/IOA/ABP/Correctness.thy \ - HOLCF/IOA/ABP/Env.thy \ - HOLCF/IOA/ABP/Impl.thy \ - HOLCF/IOA/ABP/Impl_finite.thy \ - HOLCF/IOA/ABP/Lemmas.thy \ - HOLCF/IOA/ABP/Packet.thy \ - HOLCF/IOA/ABP/ROOT.ML \ - HOLCF/IOA/ABP/Receiver.thy \ - HOLCF/IOA/ABP/Sender.thy \ - HOLCF/IOA/ABP/Spec.thy - @cd HOLCF/IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ABP - - -## IOA-NTP - -IOA-NTP: IOA $(LOG)/IOA-NTP.gz +HOLCF: + @$(ISABELLE_TOOL) build -b HOLCF -$(LOG)/IOA-NTP.gz: $(OUT)/IOA \ - HOLCF/IOA/NTP/Abschannel.thy \ - HOLCF/IOA/NTP/Action.thy \ - HOLCF/IOA/NTP/Correctness.thy \ - HOLCF/IOA/NTP/Impl.thy \ - HOLCF/IOA/NTP/Lemmas.thy \ - HOLCF/IOA/NTP/Multiset.thy \ - HOLCF/IOA/NTP/Packet.thy \ - HOLCF/IOA/NTP/ROOT.ML \ - HOLCF/IOA/NTP/Receiver.thy \ - HOLCF/IOA/NTP/Sender.thy \ - HOLCF/IOA/NTP/Spec.thy - @cd HOLCF/IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA NTP - - -## IOA-Storage - -IOA-Storage: IOA $(LOG)/IOA-Storage.gz - -$(LOG)/IOA-Storage.gz: $(OUT)/IOA \ - HOLCF/IOA/Storage/Action.thy \ - HOLCF/IOA/Storage/Correctness.thy \ - HOLCF/IOA/Storage/Impl.thy \ - HOLCF/IOA/Storage/ROOT.ML \ - HOLCF/IOA/Storage/Spec.thy - @cd HOLCF/IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA Storage - - -## IOA-ex - -IOA-ex: IOA $(LOG)/IOA-ex.gz - -$(LOG)/IOA-ex.gz: $(OUT)/IOA \ - HOLCF/IOA/ex/ROOT.ML \ - HOLCF/IOA/ex/TrivEx.thy \ - HOLCF/IOA/ex/TrivEx2.thy - @cd HOLCF/IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ex - - - -## HOL-Datatype_Benchmark - -HOL-Datatype_Benchmark: HOL $(LOG)/HOL-Datatype_Benchmark.gz - -$(LOG)/HOL-Datatype_Benchmark.gz: $(OUT)/HOL \ - Datatype_Benchmark/ROOT.ML Datatype_Benchmark/Brackin.thy \ - Datatype_Benchmark/Instructions.thy Datatype_Benchmark/SML.thy \ - Datatype_Benchmark/Verilog.thy - @$(ISABELLE_TOOL) usedir $(OUT)/HOL Datatype_Benchmark - - -## HOL-Record_Benchmark - -HOL-Record_Benchmark: HOL $(LOG)/HOL-Record_Benchmark.gz - -$(LOG)/HOL-Record_Benchmark.gz: $(OUT)/HOL Record_Benchmark/ROOT.ML \ - Record_Benchmark/Record_Benchmark.thy - @$(ISABELLE_TOOL) usedir $(OUT)/HOL Record_Benchmark - - -## HOL-Quickcheck_Benchmark - -HOL-Quickcheck_Benchmark: HOL $(LOG)/HOL-Quickcheck_Benchmark.gz - -$(LOG)/HOL-Quickcheck_Benchmark.gz: $(OUT)/HOL \ - Quickcheck_Benchmark/ROOT.ML \ - Quickcheck_Benchmark/Needham_Schroeder_Base.thy \ - Quickcheck_Benchmark/Needham_Schroeder_No_Attacker_Example.thy \ - Quickcheck_Benchmark/Needham_Schroeder_Guided_Attacker_Example.thy \ - Quickcheck_Benchmark/Needham_Schroeder_Unguided_Attacker_Example.thy \ - Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy - @$(ISABELLE_TOOL) usedir $(OUT)/HOL Quickcheck_Benchmark - - -## clean - -clean: - @rm -f $(LOG)/HOL-Algebra.gz $(LOG)/HOL-Auth.gz \ - $(LOG)/HOL-Bali.gz $(LOG)/HOL-Base.gz \ - $(LOG)/HOL-Boogie-Examples.gz $(LOG)/HOL-Boogie.gz \ - $(LOG)/HOL-Decision_Procs.gz $(LOG)/HOL-HOL_Light.gz \ - $(LOG)/HOL-Hahn_Banach.gz $(LOG)/HOL-Hoare.gz \ - $(LOG)/HOL-Hoare_Parallel.gz $(LOG)/HOL-IMP.gz \ - $(LOG)/HOL-IMPP.gz $(LOG)/HOL-IOA.gz \ - $(LOG)/HOL-Imperative_HOL.gz $(LOG)/HOL-Import.gz \ - $(LOG)/HOL-Induct.gz $(LOG)/HOL-Isar_Examples.gz \ - $(LOG)/HOL-Lattice $(LOG)/HOL-Lattice.gz \ - $(LOG)/HOL-Lex.gz $(LOG)/HOL-Library.gz \ - $(LOG)/HOL-Library-Codegenerator_Test.gz \ - $(LOG)/HOL-Main.gz $(LOG)/HOL-Matrix_LP.gz \ - $(LOG)/HOL-Metis_Examples.gz $(LOG)/HOL-MicroJava.gz \ - $(LOG)/HOL-Mirabelle.gz \ - $(LOG)/HOL-Multivariate_Analysis.gz \ - $(LOG)/HOL-Mutabelle.gz $(LOG)/HOL-NSA-Examples.gz \ - $(LOG)/HOL-NSA.gz $(LOG)/HOL-NanoJava.gz \ - $(LOG)/HOL-Nitpick_Examples.gz \ - $(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-Nominal.gz \ - $(LOG)/HOL-Number_Theory.gz \ - $(LOG)/HOL-Old_Number_Theory.gz $(LOG)/HOL-Plain.gz \ - $(LOG)/HOL-Predicate_Compile_Examples.gz \ - $(LOG)/HOL-Probability.gz $(LOG)/HOL-Prolog.gz \ - $(LOG)/HOL-Proofs.gz $(LOG)/HOL-Proofs-ex.gz \ - $(LOG)/HOL-Proofs-Extraction.gz \ - $(LOG)/HOL-Proofs-Lambda.gz \ - $(LOG)/HOL-Quickcheck_Examples.gz \ - $(LOG)/HOL-Quotient_Examples.gz \ - $(LOG)/HOL-SET_Protocol.gz \ - $(LOG)/HOL-Word-SMT_Examples.gz $(LOG)/HOL-SPARK.gz \ - $(LOG)/HOL-SPARK-Examples.gz \ - $(LOG)/HOL-SPARK-Manual.gz $(LOG)/HOL-Statespace.gz \ - $(LOG)/HOL-TPTP.gz $(LOG)/HOL-UNITY.gz \ - $(LOG)/HOL-Unix.gz $(LOG)/HOL-Word-Examples.gz \ - $(LOG)/HOL-Word.gz $(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz \ - $(LOG)/HOL.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Inc.gz \ - $(LOG)/TLA-Memory.gz $(LOG)/TLA.gz $(OUT)/HOL \ - $(OUT)/HOL-Algebra $(OUT)/HOL-Base $(OUT)/HOL-Boogie \ - $(OUT)/HOL-HOL_Light $(OUT)/HOL-IMP $(OUT)/HOL-Library \ - $(OUT)/HOL-Main $(OUT)/HOL-Multivariate_Analysis \ - $(OUT)/HOL-NSA $(OUT)/HOL-Nominal $(OUT)/HOL-Plain \ - $(OUT)/HOL-Probability $(OUT)/HOL-Proofs \ - $(OUT)/HOL-SPARK $(OUT)/HOL-Word $(OUT)/TLA \ - $(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz \ - $(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA \ - $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz \ - $(LOG)/IOA-Storage.gz $(LOG)/HOLCF-Library.gz \ - $(LOG)/IOA-ex.gz $(LOG)/HOLCF-Tutorial.gz \ - $(LOG)/HOL-Datatype_Benchmark.gz \ - $(LOG)/HOL-Record_Benchmark.gz diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Isar_Examples/ROOT.ML --- a/src/HOL/Isar_Examples/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,21 +0,0 @@ -(* Miscellaneous Isabelle/Isar examples for Higher-Order Logic. *) - -no_document use_thys ["~~/src/HOL/Library/Lattice_Syntax", "../Number_Theory/Primes"]; - -use_thys [ - "Basic_Logic", - "Cantor", - "Drinker", - "Expr_Compiler", - "Fibonacci", - "Group", - "Group_Context", - "Group_Notepad", - "Hoare_Ex", - "Knaster_Tarski", - "Mutilated_Checkerboard", - "Nested_Datatype", - "Peirce", - "Puzzle", - "Summation" -]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Lattice/ROOT.ML --- a/src/HOL/Lattice/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ -(* Title: HOL/Lattice/ROOT.ML - Author: Markus Wenzel, TU Muenchen - -Basic theory of lattices and orders. -*) - -use_thys ["CompleteLattice"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Library/ROOT.ML --- a/src/HOL/Library/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ - -(* Classical Higher-order Logic -- batteries included *) - -use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order", - "Product_Lattice", - "Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat"(*, "Code_Prolog"*), - "Code_Real_Approx_By_Float", "Target_Numeral"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Matrix_LP/ROOT.ML --- a/src/HOL/Matrix_LP/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2 +0,0 @@ - -use_thy "Cplex"; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Metis_Examples/ROOT.ML --- a/src/HOL/Metis_Examples/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -(* Title: HOL/Metis_Examples/ROOT.ML - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Author: Jasmin Blanchette, TU Muenchen - -Testing Metis and Sledgehammer. -*) - -use_thys ["Abstraction", "Big_O", "Binary_Tree", "Clausification", "Message", - "Proxies", "Tarski", "Trans_Closure", "Sets"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/MicroJava/ROOT.ML --- a/src/HOL/MicroJava/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -no_document use_thys ["~~/src/HOL/Library/While_Combinator"]; - -use_thys ["MicroJava"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Mirabelle/ROOT.ML --- a/src/HOL/Mirabelle/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -use_thys ["Mirabelle_Test"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Multivariate_Analysis/ROOT.ML --- a/src/HOL/Multivariate_Analysis/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -use_thys ["Multivariate_Analysis", "Determinants"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Mutabelle/ROOT.ML --- a/src/HOL/Mutabelle/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ - -use_thy "MutabelleExtra"; - diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/NSA/Examples/ROOT.ML --- a/src/HOL/NSA/Examples/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -use_thys ["NSPrimes"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/NSA/ROOT.ML --- a/src/HOL/NSA/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -use_thys ["Hypercomplex"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/NanoJava/ROOT.ML --- a/src/HOL/NanoJava/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -use_thys ["Example"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Nitpick_Examples/ROOT.ML --- a/src/HOL/Nitpick_Examples/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -(* Title: HOL/Nitpick_Examples/ROOT.ML - Author: Jasmin Blanchette, TU Muenchen - Copyright 2009 - -Nitpick examples. -*) - -Unsynchronized.setmp quick_and_dirty true use_thys ["Nitpick_Examples"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Nominal/Examples/ROOT.ML --- a/src/HOL/Nominal/Examples/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -use_thys ["Nominal_Examples"]; - -Unsynchronized.setmp quick_and_dirty true use_thys ["VC_Condition"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Nominal/ROOT.ML --- a/src/HOL/Nominal/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -(* Title: HOL/Nominal/ROOT.ML - Author: Stefan Berghofer and Christian Urban, TU Muenchen - -The nominal datatype package. -*) - -no_document use_thys ["~~/src/HOL/Library/Infinite_Set"]; -use_thys ["Nominal"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Number_Theory/ROOT.ML --- a/src/HOL/Number_Theory/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -use_thys ["Number_Theory"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Old_Number_Theory/ROOT.ML --- a/src/HOL/Old_Number_Theory/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,15 +0,0 @@ -no_document use_thys [ - "~~/src/HOL/Library/Infinite_Set", - "~~/src/HOL/Library/Permutation" -]; - -use_thys [ - "Fib", - "Factorization", - "Chinese", - "WilsonRuss", - "WilsonBij", - "Quadratic_Reciprocity", - "Primes", - "Pocklington" -]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Predicate_Compile_Examples/ROOT.ML --- a/src/HOL/Predicate_Compile_Examples/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,26 +0,0 @@ -use_thys [ - "Examples", - "Predicate_Compile_Tests", -(* "Predicate_Compile_Quickcheck_Examples", -- should be added again soon *) - "Specialisation_Examples" -(* "Hotel_Example_Small_Generator", - "IMP_1", - "IMP_2" - "IMP_3", - "IMP_4"*)]; - -if getenv "ISABELLE_SWIPL" = "" andalso getenv "ISABELLE_YAP" = "" then - (warning "No prolog system found - skipping some example theories"; ()) -else - if not (getenv "ISABELLE_SWIPL" = "") orelse - #1 (Isabelle_System.bash_output "\"$ISABELLE_PREDICATE_COMPILE/lib/scripts/swipl_version\"") = - "5.10.1" - then - (use_thys [ - "Code_Prolog_Examples", - "Context_Free_Grammar_Example", - "Hotel_Example_Prolog", - "Lambda_Example", - "List_Examples"]; - Unsynchronized.setmp quick_and_dirty true use_thys ["Reg_Exp_Example"]) - else (warning "Unsupported SWI-Prolog version - skipping some example theories"; ()); diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Probability/ROOT.ML --- a/src/HOL/Probability/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -no_document use_thys [ - "~~/src/HOL/Library/Countable", - "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits", - "~~/src/HOL/Library/Permutation"]; - -use_thys [ - "Probability", - "ex/Dining_Cryptographers", - "ex/Koepf_Duermuth_Countermeasure" ]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Prolog/ROOT.ML --- a/src/HOL/Prolog/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,5 +0,0 @@ -(* Title: HOL/Prolog/ROOT.ML - Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) -*) - -use_thys ["Test", "Type"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Proofs/Extraction/ROOT.ML --- a/src/HOL/Proofs/Extraction/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,11 +0,0 @@ -(* Examples for program extraction in Higher-Order Logic *) - -no_document use_thys [ - "~~/src/HOL/Library/Efficient_Nat", - "~~/src/HOL/Library/Monad_Syntax", - "~~/src/HOL/Number_Theory/Primes", - "~~/src/HOL/Number_Theory/UniqueFactorization", - "~~/src/HOL/Library/State_Monad" -]; - -use_thys ["Greatest_Common_Divisor", "Warshall", "Higman_Extraction", "Pigeonhole", "Euclid"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Proofs/Lambda/ROOT.ML --- a/src/HOL/Proofs/Lambda/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2 +0,0 @@ -no_document use_thys ["~~/src/HOL/Library/Code_Integer"]; -use_thys ["Eta", "StrongNorm", "Standardization", "WeakNorm"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Proofs/ex/ROOT.ML --- a/src/HOL/Proofs/ex/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -use_thys ["Hilbert_Classical"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Quickcheck_Benchmark/ROOT.ML --- a/src/HOL/Quickcheck_Benchmark/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,6 +0,0 @@ -Unsynchronized.setmp quick_and_dirty true use_thys [ - "Find_Unused_Assms_Examples", - "Needham_Schroeder_No_Attacker_Example", - "Needham_Schroeder_Guided_Attacker_Example", - "Needham_Schroeder_Unguided_Attacker_Example" -] diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Quickcheck_Examples/ROOT.ML --- a/src/HOL/Quickcheck_Examples/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,12 +0,0 @@ -use_thys [ - "Quickcheck_Examples" - (*, - "Quickcheck_Lattice_Examples", - "Completeness", - "Quickcheck_Interfaces", - "Hotel_Example",*) -]; - -if getenv "ISABELLE_GHC" = "" then () -else use_thy "Quickcheck_Narrowing_Examples"; - diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Quotient_Examples/ROOT.ML --- a/src/HOL/Quotient_Examples/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -(* Title: HOL/Quotient_Examples/ROOT.ML - Author: Cezary Kaliszyk and Christian Urban - -Testing the quotient package. -*) - -use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message", "Lift_FSet", - "Lift_Set", "Lift_Fun", "Quotient_Rat", "Lift_DList"]; - diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/ROOT.ML --- a/src/HOL/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,4 +0,0 @@ - -(* Classical Higher-order Logic *) - -use_thys ["Complex_Main"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Record_Benchmark/ROOT.ML --- a/src/HOL/Record_Benchmark/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -(* Title: HOL/Record_Benchmark/ROOT.ML - -Some benchmark on large record. -*) - -Toplevel.timing := true; - -use_thys ["Record_Benchmark"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/SET_Protocol/ROOT.ML --- a/src/HOL/SET_Protocol/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2 +0,0 @@ -no_document use_thys ["~~/src/HOL/Library/Nat_Bijection"]; -use_thys ["SET_Protocol"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/SMT_Examples/ROOT.ML --- a/src/HOL/SMT_Examples/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2 +0,0 @@ -quick_and_dirty := true; -use_thys ["SMT_Tests", "SMT_Examples", "SMT_Word_Examples"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/SPARK/Examples/ROOT.ML --- a/src/HOL/SPARK/Examples/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,16 +0,0 @@ -use_thys - ["Gcd/Greatest_Common_Divisor", - - "Liseq/Longest_Increasing_Subsequence", - - "RIPEMD-160/F", - "RIPEMD-160/Hash", - "RIPEMD-160/K_L", - "RIPEMD-160/K_R", - "RIPEMD-160/R_L", - "RIPEMD-160/Round", - "RIPEMD-160/R_R", - "RIPEMD-160/S_L", - "RIPEMD-160/S_R", - - "Sqrt/Sqrt"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/SPARK/Manual/ROOT.ML --- a/src/HOL/SPARK/Manual/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ -Printer.show_question_marks_default := false; - -use_thys - ["Example_Verification", - "VC_Principles", - "Reference", - "Complex_Types"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/SPARK/ROOT.ML --- a/src/HOL/SPARK/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -use_thys ["SPARK"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Statespace/ROOT.ML --- a/src/HOL/Statespace/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -use_thys ["StateSpaceEx"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/TLA/Buffer/ROOT.ML --- a/src/HOL/TLA/Buffer/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -use_thys ["DBuffer"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/TLA/Inc/ROOT.ML --- a/src/HOL/TLA/Inc/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -use_thys ["Inc"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/TLA/Memory/ROOT.ML --- a/src/HOL/TLA/Memory/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -use_thys ["MemoryImplementation"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/TLA/ROOT.ML --- a/src/HOL/TLA/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -(* The Temporal Logic of Actions *) - -use_thys ["TLA"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/TPTP/ROOT.ML --- a/src/HOL/TPTP/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,18 +0,0 @@ -(* Title: HOL/TPTP/ROOT.ML - Author: Jasmin Blanchette, TU Muenchen - Author: Nik Sultana, University of Cambridge - Copyright 2011 - -TPTP-related extensions. -*) - -use_thys [ - "ATP_Theory_Export", - "MaSh_Eval", - "MaSh_Export", - "TPTP_Interpret", - "THF_Arith" -]; - -Unsynchronized.setmp Proofterm.proofs (!Proofterm.proofs) - use_thy "ATP_Problem_Import"; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/UNITY/ROOT.ML --- a/src/HOL/UNITY/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,43 +0,0 @@ -(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge -*) - -(*Verifying security protocols using UNITY*) -no_document use_thys ["../Auth/Public"]; - -use_thys [ - (*Basic meta-theory*) - "UNITY_Main", - - (*Simple examples: no composition*) - "Simple/Deadlock", - "Simple/Common", - "Simple/Network", - "Simple/Token", - "Simple/Channel", - "Simple/Lift", - "Simple/Mutex", - "Simple/Reach", - "Simple/Reachability", - - (*Verifying security protocols using UNITY*) - "Simple/NSP_Bad", - - (*Example of composition*) - "Comp/Handshake", - - (*Universal properties examples*) - "Comp/Counter", - "Comp/Counterc", - "Comp/Priority", - - "Comp/TimerArray", - "Comp/Progress", - - "Comp/Alloc", - "Comp/AllocImpl", - "Comp/Client", - - (*obsolete*) - "ELT" -]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Unix/ROOT.ML --- a/src/HOL/Unix/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -use_thys ["Unix"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Word/Examples/ROOT.ML --- a/src/HOL/Word/Examples/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -use_thys ["WordExamples"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/Word/ROOT.ML --- a/src/HOL/Word/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -use_thys ["Word"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/ZF/ROOT.ML --- a/src/HOL/ZF/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -use_thys ["MainZF", "Games"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,90 +0,0 @@ -(* Title: HOL/ex/ROOT.ML - -Miscellaneous examples for Higher-Order Logic. -*) - -no_document use_thys [ - "~~/src/HOL/Library/State_Monad", - "Code_Nat_examples", - "~~/src/HOL/Library/FuncSet", - "Eval_Examples", - "Normalization_by_Evaluation", - "Hebrew", - "Chinese", - "Serbian", - "~~/src/HOL/Library/FinFun_Syntax" -]; - -use_thys [ - "Iff_Oracle", - "Coercion_Examples", - "Numeral_Representation", - "Higher_Order_Logic", - "Abstract_NAT", - "Guess", - "Binary", - "Fundefs", - "Induction_Schema", - "LocaleTest2", - "Records", - "While_Combinator_Example", - "MonoidGroup", - "BinEx", - "Hex_Bin_Examples", - "Antiquote", - "Multiquote", - "PER", - "NatSum", - "ThreeDivides", - "Intuitionistic", - "CTL", - "Arith_Examples", - "BT", - "Tree23", - "MergeSort", - "Lagrange", - "Groebner_Examples", - "MT", - "Unification", - "Primrec", - "Tarski", - "Classical", - "Set_Theory", - "Meson_Test", - "Termination", - "Coherent", - "PresburgerEx", - "ReflectionEx", - "Sqrt", - "Sqrt_Script", - "Transfer_Ex", - "Transfer_Int_Nat", - "HarmonicSeries", - "Refute_Examples", - "Landau", - "Execute_Choice", - "Summation", - "Gauge_Integration", - "Dedekind_Real", - "Quicksort", - "Birthday_Paradox", - "List_to_Set_Comprehension_Examples", - "Seq", - "Simproc_Tests", - "Executable_Relation", - "FinFunPred", - "Set_Comprehension_Pointfree_Tests", - "Parallel_Example" -]; - -use_thy "SVC_Oracle"; -if getenv "SVC_HOME" = "" then () -else use_thy "svc_test"; - -(*requires zChaff (or some other reasonably fast SAT solver)*) -if getenv "ZCHAFF_HOME" = "" then () -else use_thy "Sudoku"; - -(*requires a proof-generating SAT solver (zChaff or MiniSAT)*) -(*global side-effects ahead!*) -try use_thy "SAT_Examples"; (* FIXME try!? (not really a proper test) *) diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/LCF/IsaMakefile --- a/src/LCF/IsaMakefile Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,44 +0,0 @@ -# -# IsaMakefile for LCF -# - -## targets - -default: LCF -images: LCF -test: LCF-ex -all: images test -full: all -smlnj: all - - -## global settings - -SRC = $(ISABELLE_HOME)/src -OUT = $(ISABELLE_OUTPUT) -LOG = $(OUT)/log - - -## LCF - -LCF: FOL $(OUT)/LCF - -FOL: - @cd $(SRC)/FOL; $(ISABELLE_TOOL) make FOL - -$(OUT)/LCF: $(OUT)/FOL LCF.thy ROOT.ML - @$(ISABELLE_TOOL) usedir -b -r $(OUT)/FOL LCF - - -## LCF-ex - -LCF-ex: LCF $(LOG)/LCF-ex.gz - -$(LOG)/LCF-ex.gz: $(OUT)/LCF ex/Ex1.thy ex/Ex2.thy ex/Ex3.thy ex/Ex4.thy ex/ROOT.ML - @$(ISABELLE_TOOL) usedir $(OUT)/LCF ex - - -## clean - -clean: - @rm -f $(OUT)/LCF $(LOG)/LCF.gz $(LOG)/LCF-ex.gz diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/LCF/ROOT.ML --- a/src/LCF/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ -(* Title: LCF/ROOT.ML - Author: Tobias Nipkow - Copyright 1992 University of Cambridge -*) - -use_thys ["LCF"]; - diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/LCF/ex/ROOT.ML --- a/src/LCF/ex/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -(* Title: LCF/ex/ROOT.ML - Author: Tobias Nipkow - Copyright 1991 University of Cambridge - -Some examples from Lawrence Paulson's book Logic and Computation. -*) - -use_thys ["Ex1", "Ex2", "Ex3", "Ex4"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,270 +0,0 @@ -# -# IsaMakefile for Pure -# - -## targets - -default: Pure -images: Pure -test: RAW -all: images test -full: all -smlnj: all - - -## global settings - -SRC = $(ISABELLE_HOME)/src -OUT = $(ISABELLE_OUTPUT) -LOG = $(OUT)/log - - -## Pure - -BOOTSTRAP_FILES = \ - General/exn.ML \ - ML-Systems/compiler_polyml.ML \ - ML-Systems/ml_name_space.ML \ - ML-Systems/ml_pretty.ML \ - ML-Systems/ml_system.ML \ - ML-Systems/multithreading.ML \ - ML-Systems/multithreading_polyml.ML \ - ML-Systems/overloading_smlnj.ML \ - ML-Systems/polyml.ML \ - ML-Systems/pp_dummy.ML \ - ML-Systems/proper_int.ML \ - ML-Systems/single_assignment.ML \ - ML-Systems/single_assignment_polyml.ML \ - ML-Systems/smlnj.ML \ - ML-Systems/thread_dummy.ML \ - ML-Systems/universal.ML \ - ML-Systems/unsynchronized.ML \ - ML-Systems/use_context.ML - -RAW: $(OUT)/RAW - -$(OUT)/RAW: $(BOOTSTRAP_FILES) - @./mk -r - - -Pure: $(OUT)/Pure - -$(OUT)/Pure: $(BOOTSTRAP_FILES) \ - Concurrent/bash.ML \ - Concurrent/bash_sequential.ML \ - Concurrent/cache.ML \ - Concurrent/future.ML \ - Concurrent/lazy.ML \ - Concurrent/lazy_sequential.ML \ - Concurrent/mailbox.ML \ - Concurrent/par_exn.ML \ - Concurrent/par_list.ML \ - Concurrent/par_list_sequential.ML \ - Concurrent/simple_thread.ML \ - Concurrent/single_assignment.ML \ - Concurrent/single_assignment_sequential.ML \ - Concurrent/synchronized.ML \ - Concurrent/synchronized_sequential.ML \ - Concurrent/task_queue.ML \ - Concurrent/time_limit.ML \ - General/alist.ML \ - General/antiquote.ML \ - General/balanced_tree.ML \ - General/basics.ML \ - General/binding.ML \ - General/buffer.ML \ - General/file.ML \ - General/graph.ML \ - General/heap.ML \ - General/integer.ML \ - General/linear_set.ML \ - General/long_name.ML \ - General/name_space.ML \ - General/ord_list.ML \ - General/output.ML \ - General/path.ML \ - General/position.ML \ - General/pretty.ML \ - General/print_mode.ML \ - General/properties.ML \ - General/queue.ML \ - General/same.ML \ - General/scan.ML \ - General/secure.ML \ - General/seq.ML \ - General/sha1.ML \ - General/sha1_polyml.ML \ - General/source.ML \ - General/stack.ML \ - General/symbol.ML \ - General/symbol_pos.ML \ - General/table.ML \ - General/timing.ML \ - General/url.ML \ - Isar/args.ML \ - Isar/attrib.ML \ - Isar/auto_bind.ML \ - Isar/bundle.ML \ - Isar/calculation.ML \ - Isar/class.ML \ - Isar/class_declaration.ML \ - Isar/code.ML \ - Isar/context_rules.ML \ - Isar/element.ML \ - Isar/expression.ML \ - Isar/generic_target.ML \ - Isar/isar_cmd.ML \ - Isar/isar_syn.ML \ - Isar/keyword.ML \ - Isar/local_defs.ML \ - Isar/local_theory.ML \ - Isar/locale.ML \ - Isar/method.ML \ - Isar/named_target.ML \ - Isar/object_logic.ML \ - Isar/obtain.ML \ - Isar/outer_syntax.ML \ - Isar/overloading.ML \ - Isar/parse.ML \ - Isar/parse_spec.ML \ - Isar/proof.ML \ - Isar/proof_context.ML \ - Isar/proof_display.ML \ - Isar/proof_node.ML \ - Isar/rule_cases.ML \ - Isar/rule_insts.ML \ - Isar/runtime.ML \ - Isar/skip_proof.ML \ - Isar/spec_rules.ML \ - Isar/specification.ML \ - Isar/token.ML \ - Isar/toplevel.ML \ - Isar/typedecl.ML \ - ML/install_pp_polyml.ML \ - ML/ml_antiquote.ML \ - ML/ml_compiler.ML \ - ML/ml_compiler_polyml.ML \ - ML/ml_context.ML \ - ML/ml_env.ML \ - ML/ml_lex.ML \ - ML/ml_parse.ML \ - ML/ml_syntax.ML \ - ML/ml_thms.ML \ - PIDE/command.ML \ - PIDE/document.ML \ - PIDE/isabelle_markup.ML \ - PIDE/markup.ML \ - PIDE/protocol.ML \ - PIDE/xml.ML \ - PIDE/yxml.ML \ - Proof/extraction.ML \ - Proof/proof_checker.ML \ - Proof/proof_rewrite_rules.ML \ - Proof/proof_syntax.ML \ - Proof/reconstruct.ML \ - ProofGeneral/pgip.ML \ - ProofGeneral/pgip_input.ML \ - ProofGeneral/pgip_isabelle.ML \ - ProofGeneral/pgip_markup.ML \ - ProofGeneral/pgip_output.ML \ - ProofGeneral/pgip_parser.ML \ - ProofGeneral/pgip_tests.ML \ - ProofGeneral/pgip_types.ML \ - ProofGeneral/pgml.ML \ - ProofGeneral/preferences.ML \ - ProofGeneral/proof_general_emacs.ML \ - ProofGeneral/proof_general_pgip.ML \ - Pure.thy \ - ROOT.ML \ - Syntax/ast.ML \ - Syntax/lexicon.ML \ - Syntax/local_syntax.ML \ - Syntax/mixfix.ML \ - Syntax/parser.ML \ - Syntax/printer.ML \ - Syntax/simple_syntax.ML \ - Syntax/syntax.ML \ - Syntax/syntax_ext.ML \ - Syntax/syntax_phases.ML \ - Syntax/syntax_trans.ML \ - Syntax/term_position.ML \ - System/build.ML \ - System/command_line.ML \ - System/invoke_scala.ML \ - System/isabelle_process.ML \ - System/isabelle_system.ML \ - System/isar.ML \ - System/options.ML \ - System/session.ML \ - System/system_channel.ML \ - Thy/html.ML \ - Thy/latex.ML \ - Thy/present.ML \ - Thy/rail.ML \ - Thy/term_style.ML \ - Thy/thm_deps.ML \ - Thy/thy_header.ML \ - Thy/thy_info.ML \ - Thy/thy_load.ML \ - Thy/thy_output.ML \ - Thy/thy_syntax.ML \ - Tools/find_consts.ML \ - Tools/find_theorems.ML \ - Tools/named_thms.ML \ - Tools/xml_syntax.ML \ - assumption.ML \ - axclass.ML \ - config.ML \ - conjunction.ML \ - consts.ML \ - context.ML \ - context_position.ML \ - conv.ML \ - defs.ML \ - display.ML \ - drule.ML \ - envir.ML \ - facts.ML \ - global_theory.ML \ - goal.ML \ - goal_display.ML \ - interpretation.ML \ - item_net.ML \ - library.ML \ - logic.ML \ - more_thm.ML \ - morphism.ML \ - name.ML \ - net.ML \ - pattern.ML \ - primitive_defs.ML \ - proofterm.ML \ - pure_setup.ML \ - pure_thy.ML \ - raw_simplifier.ML \ - search.ML \ - sign.ML \ - simplifier.ML \ - sorts.ML \ - subgoal.ML \ - tactic.ML \ - tactical.ML \ - term.ML \ - term_ord.ML \ - term_sharing.ML \ - term_subst.ML \ - term_xml.ML \ - theory.ML \ - thm.ML \ - type.ML \ - type_infer.ML \ - type_infer_context.ML \ - unify.ML \ - variable.ML - @./mk - - -## clean - -clean: - @rm -f $(OUT)/Pure $(LOG)/Pure.gz $(OUT)/RAW $(LOG)/RAW.gz diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/Sequents/IsaMakefile --- a/src/Sequents/IsaMakefile Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,47 +0,0 @@ -# -# IsaMakefile for Sequents -# - -## targets - -default: Sequents -images: Sequents -test: Sequents-LK -all: images test -full: all -smlnj: all - - -## global settings - -SRC = $(ISABELLE_HOME)/src -OUT = $(ISABELLE_OUTPUT) -LOG = $(OUT)/log - - -## Sequents - -Sequents: Pure $(OUT)/Sequents - -Pure: - @cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure - -$(OUT)/Sequents: $(OUT)/Pure ILL.thy LK0.thy LK.thy \ - modal.ML ROOT.ML simpdata.ML S4.thy S43.thy Sequents.thy T.thy prover.ML \ - ILL_predlog.thy Washing.thy - @$(ISABELLE_TOOL) usedir -b $(OUT)/Pure Sequents - - -## Sequents-LK - -Sequents-LK: Sequents $(LOG)/Sequents-LK.gz - -$(LOG)/Sequents-LK.gz: $(OUT)/Sequents LK/ROOT.ML LK/Hard_Quantifiers.thy \ - LK/Propositional.thy LK/Quantifiers.thy LK/Nat.thy - @$(ISABELLE_TOOL) usedir $(OUT)/Sequents LK - - -## clean - -clean: - @rm -f $(OUT)/Sequents $(LOG)/Sequents.gz $(LOG)/Sequents-LK.gz diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/Sequents/LK/ROOT.ML --- a/src/Sequents/LK/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -(* Title: Sequents/LK/ROOT.ML - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1992 University of Cambridge - -Examples for Classical Logic. -*) - -use_thys ["Propositional", "Quantifiers", "Hard_Quantifiers", "Nat"]; - diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/Sequents/ROOT.ML --- a/src/Sequents/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -(* Title: Sequents/ROOT.ML - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1991 University of Cambridge - -Classical Sequent Calculus based on Pure Isabelle. -*) - -use_thys ["LK", "ILL", "ILL_predlog", "Washing", "Modal0", "T", "S4", "S43"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/Tools/WWW_Find/IsaMakefile --- a/src/Tools/WWW_Find/IsaMakefile Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,42 +0,0 @@ -# -# IsaMakefile for WWW_Find -# -# Provides static compile check for ML files only. - -## targets - -default: Pure-WWW_Find -images: -test: Pure-WWW_Find -all: images test -full: all -smlnj: all - - -## global settings - -SRC = $(ISABELLE_HOME)/src -OUT = $(ISABELLE_OUTPUT) -LOG = $(OUT)/log - - -## Pure-WWW_Find - -LOGFILE = $(LOG)/Pure-WWW_Find.gz - -Pure-WWW_Find: Pure $(LOGFILE) - -Pure: - @cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure - -$(LOGFILE): $(OUT)/Pure echo.ML find_theorems.ML html_unicode.ML \ - html_templates.ML http_status.ML http_util.ML mime.ML scgi_req.ML \ - scgi_server.ML socket_util.ML unicode_symbols.ML xhtml.ML \ - yxml_find_theorems.ML ROOT.ML - @cd ..; $(ISABELLE_TOOL) usedir Pure WWW_Find - - -## clean - -clean: - @rm -f $(LOGFILE) diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/Tools/WWW_Find/ROOT.ML --- a/src/Tools/WWW_Find/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -if ML_System.is_polyml then use_thy "WWW_Find" -else (); - diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/ZF/AC/ROOT.ML --- a/src/ZF/AC/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -(* Title: ZF/AC/ROOT.ML - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1995 University of Cambridge - -Proofs of AC-equivalences, due to Krzysztof Grabczewski. -*) - -use_thys ["WO6_WO1", "WO1_WO7", "AC7_AC9", "WO1_AC", "AC15_WO6", - "WO2_AC16", "AC16_WO4", "AC17_AC1", "AC18_AC19", "DC"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/ZF/Coind/ROOT.ML --- a/src/ZF/Coind/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,15 +0,0 @@ -(* Title: ZF/Coind/ROOT.ML - Author: Jacob Frost, Cambridge University Computer Laboratory - Copyright 1995 University of Cambridge - -Based upon the article - Robin Milner and Mads Tofte, - Co-induction in Relational Semantics, - Theoretical Computer Science 87 (1991), pages 209-220. - -Written up as - Jacob Frost, A Case Study of Co_induction in Isabelle - Report, Computer Lab, University of Cambridge (1995). -*) - -use_thys ["ECR"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/ZF/Constructible/ROOT.ML --- a/src/ZF/Constructible/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -(* Title: ZF/Constructible/ROOT.ML - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 2002 University of Cambridge - -Inner Models, Absoluteness and Consistency Proofs. -*) - -use_thys ["DPow_absolute", "AC_in_L", "Rank_Separation"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/ZF/IMP/ROOT.ML --- a/src/ZF/IMP/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,14 +0,0 @@ -(* Title: ZF/IMP/ROOT.ML - Author: Heiko Loetzbeyer & Robert Sandner, TUM - Copyright 1994 TUM - -Executes the formalization of the denotational and operational semantics of a -simple while-language, including an equivalence proof. The whole development -essentially formalizes/transcribes chapters 2 and 5 of - -Glynn Winskel. The Formal Semantics of Programming Languages. -MIT Press, 1993. - -*) - -use_thys ["Equiv"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/ZF/Induct/ROOT.ML --- a/src/ZF/Induct/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,30 +0,0 @@ -(* Title: ZF/Induct/ROOT.ML - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 2001 University of Cambridge - -Inductive definitions. -*) - -use_thys [ -(** Datatypes **) - "Datatypes", (*sample datatypes*) - "Binary_Trees", (*binary trees*) - "Term", (*recursion over the list functor*) - "Ntree", (*variable-branching trees; function demo*) - "Tree_Forest", (*mutual recursion*) - "Brouwer", (*Infinite-branching trees*) - "Mutil", (*mutilated chess board*) - -(*by Sidi Ehmety: Multisets. A parent is FoldSet, the "fold" function for -finite sets*) - "Multiset", - "Rmap", (*mapping a relation over a list*) - "PropLog", (*completeness of propositional logic*) - -(*two Coq examples by Christine Paulin-Mohring*) - "ListN", - "Acc", - - "Comb", (*Combinatory Logic example*) - "Primrec" (*Primitive recursive functions*) -]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/ZF/IsaMakefile --- a/src/ZF/IsaMakefile Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,149 +0,0 @@ -# -# IsaMakefile for ZF -# - -## targets - -default: ZF -images: ZF - -#Note: keep targets sorted -test: ZF-AC ZF-Coind ZF-Constructible ZF-IMP ZF-Induct ZF-Resid ZF-UNITY ZF-ex -all: images test -full: all -smlnj: all - - -## global settings - -SRC = $(ISABELLE_HOME)/src -OUT = $(ISABELLE_OUTPUT) -LOG = $(OUT)/log - - -## ZF - -ZF: FOL $(OUT)/ZF - -FOL: - @cd $(SRC)/FOL; $(ISABELLE_TOOL) make FOL - -$(OUT)/ZF: $(OUT)/FOL AC.thy Arith.thy ArithSimp.thy Bin.thy Bool.thy \ - Cardinal.thy CardinalArith.thy Cardinal_AC.thy Datatype_ZF.thy \ - Epsilon.thy EquivClass.thy Finite.thy Fixedpt.thy Inductive_ZF.thy \ - InfDatatype.thy Int_ZF.thy IntArith.thy IntDiv_ZF.thy List_ZF.thy \ - Main.thy Main_ZF.thy Main_ZFC.thy Nat_ZF.thy OrdQuant.thy Order.thy \ - OrderArith.thy OrderType.thy Ordinal.thy Perm.thy QPair.thy \ - QUniv.thy ROOT.ML Sum.thy Tools/cartprod.ML \ - Tools/datatype_package.ML Tools/ind_cases.ML Tools/induct_tacs.ML \ - Tools/inductive_package.ML Tools/numeral_syntax.ML \ - Tools/primrec_package.ML Tools/typechk.ML Trancl.thy Univ.thy WF.thy \ - ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy ind_syntax.ML \ - int_arith.ML pair.thy simpdata.ML upair.thy - @$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/FOL ZF - - -## ZF-AC - -ZF-AC: ZF $(LOG)/ZF-AC.gz - -$(LOG)/ZF-AC.gz: $(OUT)/ZF AC/ROOT.ML AC/AC15_WO6.thy AC/AC16_WO4.thy \ - AC/AC16_lemmas.thy AC/AC17_AC1.thy AC/AC18_AC19.thy AC/AC7_AC9.thy \ - AC/AC_Equiv.thy AC/Cardinal_aux.thy AC/DC.thy AC/HH.thy \ - AC/Hartog.thy AC/WO1_AC.thy AC/WO1_WO7.thy AC/WO2_AC16.thy \ - AC/WO6_WO1.thy AC/document/root.bib AC/document/root.tex - @$(ISABELLE_TOOL) usedir -g true $(OUT)/ZF AC - - -## ZF-Coind - -ZF-Coind: ZF $(LOG)/ZF-Coind.gz - -$(LOG)/ZF-Coind.gz: $(OUT)/ZF Coind/Dynamic.thy Coind/ECR.thy \ - Coind/Language.thy Coind/Map.thy Coind/ROOT.ML Coind/Static.thy \ - Coind/Types.thy Coind/Values.thy - @$(ISABELLE_TOOL) usedir $(OUT)/ZF Coind - - -## ZF-Constructible - -ZF-Constructible: ZF $(LOG)/ZF-Constructible.gz - -$(LOG)/ZF-Constructible.gz: $(OUT)/ZF Constructible/ROOT.ML \ - Constructible/Datatype_absolute.thy Constructible/DPow_absolute.thy \ - Constructible/Formula.thy Constructible/Internalize.thy \ - Constructible/AC_in_L.thy Constructible/Relative.thy \ - Constructible/L_axioms.thy Constructible/Wellorderings.thy \ - Constructible/MetaExists.thy Constructible/Normal.thy \ - Constructible/Rank.thy Constructible/Rank_Separation.thy \ - Constructible/Rec_Separation.thy Constructible/Separation.thy \ - Constructible/Satisfies_absolute.thy Constructible/WF_absolute.thy \ - Constructible/Reflection.thy Constructible/WFrec.thy \ - Constructible/document/root.bib Constructible/document/root.tex - @$(ISABELLE_TOOL) usedir -g true $(OUT)/ZF Constructible - - -## ZF-IMP - -ZF-IMP: ZF $(LOG)/ZF-IMP.gz - -$(LOG)/ZF-IMP.gz: $(OUT)/ZF IMP/Com.thy IMP/Denotation.thy \ - IMP/Equiv.thy IMP/ROOT.ML IMP/document/root.bib \ - IMP/document/root.tex - @$(ISABELLE_TOOL) usedir $(OUT)/ZF IMP - - -## ZF-Resid - -ZF-Resid: ZF $(LOG)/ZF-Resid.gz - -$(LOG)/ZF-Resid.gz: $(OUT)/ZF Resid/ROOT.ML Resid/Confluence.thy \ - Resid/Redex.thy Resid/Reduction.thy Resid/Residuals.thy \ - Resid/Substitution.thy - @$(ISABELLE_TOOL) usedir $(OUT)/ZF Resid - - -## ZF-UNITY - -ZF-UNITY: ZF $(LOG)/ZF-UNITY.gz - -$(LOG)/ZF-UNITY.gz: $(OUT)/ZF UNITY/ROOT.ML UNITY/Comp.thy \ - UNITY/Constrains.thy UNITY/FP.thy UNITY/GenPrefix.thy UNITY/Guar.thy \ - UNITY/Mutex.thy UNITY/State.thy UNITY/SubstAx.thy UNITY/UNITY.thy \ - UNITY/Union.thy UNITY/AllocBase.thy UNITY/AllocImpl.thy \ - UNITY/ClientImpl.thy UNITY/Distributor.thy UNITY/Follows.thy \ - UNITY/Increasing.thy UNITY/Merge.thy UNITY/Monotonicity.thy \ - UNITY/MultisetSum.thy UNITY/WFair.thy - @$(ISABELLE_TOOL) usedir $(OUT)/ZF UNITY - - -## ZF-Induct - -ZF-Induct: ZF $(LOG)/ZF-Induct.gz - -$(LOG)/ZF-Induct.gz: $(OUT)/ZF Induct/ROOT.ML Induct/Acc.thy \ - Induct/Binary_Trees.thy Induct/Brouwer.thy Induct/Comb.thy \ - Induct/Datatypes.thy Induct/FoldSet.thy Induct/ListN.thy \ - Induct/Multiset.thy Induct/Mutil.thy Induct/Ntree.thy \ - Induct/Primrec.thy Induct/PropLog.thy Induct/Rmap.thy \ - Induct/Term.thy Induct/Tree_Forest.thy Induct/document/root.tex - @$(ISABELLE_TOOL) usedir $(OUT)/ZF Induct - - -## ZF-ex - -ZF-ex: ZF $(LOG)/ZF-ex.gz - -$(LOG)/ZF-ex.gz: $(OUT)/ZF ex/ROOT.ML ex/BinEx.thy ex/CoUnit.thy \ - ex/Commutation.thy ex/Group.thy ex/Limit.thy ex/LList.thy \ - ex/Primes.thy ex/NatSum.thy ex/Ramsey.thy ex/Ring.thy ex/misc.thy - @$(ISABELLE_TOOL) usedir $(OUT)/ZF ex - - -## clean - -clean: - @rm -f $(OUT)/ZF $(LOG)/ZF.gz $(LOG)/ZF-AC.gz \ - $(LOG)/ZF-Coind.gz $(LOG)/ZF-Constructible.gz \ - $(LOG)/ZF-ex.gz $(LOG)/ZF-IMP.gz $(LOG)/ZF-Induct.gz \ - $(LOG)/ZF-Resid.gz $(LOG)/ZF-UNITY.gz diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/ZF/ROOT.ML --- a/src/ZF/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,11 +0,0 @@ -(* Title: ZF/ROOT.ML - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -Zermelo-Fraenkel Set Theory on top of classical First-Order Logic. -This theory is the work of Martin Coen, Philippe Noel and Lawrence -Paulson. -*) - -use_thys ["Main", "Main_ZFC"]; - diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/ZF/Resid/ROOT.ML --- a/src/ZF/Resid/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,14 +0,0 @@ -(* Title: ZF/Resid/ROOT.ML - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1995 University of Cambridge - -Executes the Residuals example. -This is a proof of the Church-Rosser Theorem for the untyped lambda-calculus. - -By Ole Rasmussen, following the Coq proof given in - -Gerard Huet. Residual Theory in Lambda-Calculus: A Formal Development. -J. Functional Programming 4(3) 1994, 371-394. -*) - -use_thys ["Confluence"]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/ZF/UNITY/ROOT.ML --- a/src/ZF/UNITY/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,17 +0,0 @@ -(* Title: ZF/UNITY/ROOT.ML - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -ZF/UNITY proofs. -*) - -use_thys [ - (*Simple examples: no composition*) - "Mutex", - - (*Basic meta-theory*) - "Guar", - - (*Prefix relation; the Allocator example*) - "Distributor", "Merge", "ClientImpl", "AllocImpl" -]; diff -r 866f6d5baf4c -r a5e3ba7cbb2a src/ZF/ex/ROOT.ML --- a/src/ZF/ex/ROOT.ML Tue Aug 07 23:38:18 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,18 +0,0 @@ -(* Title: ZF/ex/ROOT.ML - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -Miscellaneous examples for Zermelo-Fraenkel Set Theory. -*) - -use_thys [ - "misc", - "Ring", (*abstract algebra*) - "Commutation", (*abstract Church-Rosser theory*) - "Primes", (*GCD theory*) - "NatSum", (*Summing integers, squares, cubes, etc.*) - "Ramsey", (*Simple form of Ramsey's theorem*) - "Limit", (*Inverse limit construction of domains*) - "BinEx", (*Binary integer arithmetic*) - "LList", "CoUnit" (*CoDatatypes*) -];