src/HOL/IsaMakefile
changeset 33270 320a1d67b9ae
parent 33269 3b7e2dbbd684
parent 33210 94ae82a4452f
child 33271 7be66dee1a5a
     1.1 --- a/src/HOL/IsaMakefile	Tue Oct 27 12:59:57 2009 +0000
     1.2 +++ b/src/HOL/IsaMakefile	Tue Oct 27 14:46:03 2009 +0000
     1.3 @@ -6,7 +6,20 @@
     1.4  
     1.5  default: HOL
     1.6  generate: HOL-Generate-HOL HOL-Generate-HOLLight
     1.7 -images: HOL HOL-Base HOL-Plain HOL-Main HOL-Algebra HOL-Nominal HOL-NSA HOL-SMT HOL-Word TLA HOL4
     1.8 +
     1.9 +images: \
    1.10 +  HOL \
    1.11 +  HOL-Algebra \
    1.12 +  HOL-Base \
    1.13 +  HOL-Main \
    1.14 +  HOL-Multivariate_Analysis \
    1.15 +  HOL-NSA \
    1.16 +  HOL-Nominal \
    1.17 +  HOL-Plain \
    1.18 +  HOL-SMT \
    1.19 +  HOL-Word \
    1.20 +  HOL4 \
    1.21 +  TLA
    1.22  
    1.23  #Note: keep targets sorted (except for HOL-Library and HOL-ex)
    1.24  test: \
    1.25 @@ -19,11 +32,11 @@
    1.26    HOL-Hahn_Banach \
    1.27    HOL-Hoare \
    1.28    HOL-Hoare_Parallel \
    1.29 -  HOL-Import \
    1.30    HOL-IMP \
    1.31    HOL-IMPP \
    1.32    HOL-IOA \
    1.33    HOL-Imperative_HOL \
    1.34 +  HOL-Import \
    1.35    HOL-Induct \
    1.36    HOL-Isar_Examples \
    1.37    HOL-Lambda \
    1.38 @@ -34,13 +47,14 @@
    1.39    HOL-Mirabelle \
    1.40    HOL-Modelcheck \
    1.41    HOL-NanoJava \
    1.42 +  HOL-Nitpick_Examples \
    1.43    HOL-Nominal-Examples \
    1.44    HOL-Number_Theory \
    1.45    HOL-Old_Number_Theory \
    1.46    HOL-Prolog \
    1.47    HOL-SET_Protocol \
    1.48 +  HOL-SMT-Examples \
    1.49    HOL-SizeChange \
    1.50 -  HOL-SMT-Examples \
    1.51    HOL-Statespace \
    1.52    HOL-Subst \
    1.53        TLA-Buffer \
    1.54 @@ -131,6 +145,7 @@
    1.55    Inductive.thy \
    1.56    Lattices.thy \
    1.57    Nat.thy \
    1.58 +  Nitpick.thy \
    1.59    Option.thy \
    1.60    OrderedGroup.thy \
    1.61    Orderings.thy \
    1.62 @@ -156,15 +171,14 @@
    1.63    Tools/Datatype/datatype_realizer.ML \
    1.64    Tools/Datatype/datatype_rep_proofs.ML \
    1.65    Tools/dseq.ML \
    1.66 -  Tools/Function/auto_term.ML \
    1.67    Tools/Function/context_tree.ML \
    1.68    Tools/Function/decompose.ML \
    1.69    Tools/Function/descent.ML \
    1.70 -  Tools/Function/fundef_common.ML \
    1.71 -  Tools/Function/fundef_core.ML \
    1.72 -  Tools/Function/fundef_datatype.ML \
    1.73 -  Tools/Function/fundef_lib.ML \
    1.74 -  Tools/Function/fundef.ML \
    1.75 +  Tools/Function/function_common.ML \
    1.76 +  Tools/Function/function_core.ML \
    1.77 +  Tools/Function/function_lib.ML \
    1.78 +  Tools/Function/function.ML \
    1.79 +  Tools/Function/fun.ML \
    1.80    Tools/Function/induction_scheme.ML \
    1.81    Tools/Function/inductive_wrap.ML \
    1.82    Tools/Function/lexicographic_order.ML \
    1.83 @@ -172,11 +186,27 @@
    1.84    Tools/Function/mutual.ML \
    1.85    Tools/Function/pat_completeness.ML \
    1.86    Tools/Function/pattern_split.ML \
    1.87 +  Tools/Function/relation.ML \
    1.88    Tools/Function/scnp_reconstruct.ML \
    1.89    Tools/Function/scnp_solve.ML \
    1.90    Tools/Function/size.ML \
    1.91    Tools/Function/sum_tree.ML \
    1.92    Tools/Function/termination.ML \
    1.93 +  Tools/Nitpick/kodkod.ML \
    1.94 +  Tools/Nitpick/kodkod_sat.ML \
    1.95 +  Tools/Nitpick/minipick.ML \
    1.96 +  Tools/Nitpick/nitpick.ML \
    1.97 +  Tools/Nitpick/nitpick_hol.ML \
    1.98 +  Tools/Nitpick/nitpick_isar.ML \
    1.99 +  Tools/Nitpick/nitpick_kodkod.ML \
   1.100 +  Tools/Nitpick/nitpick_model.ML \
   1.101 +  Tools/Nitpick/nitpick_mono.ML \
   1.102 +  Tools/Nitpick/nitpick_nut.ML \
   1.103 +  Tools/Nitpick/nitpick_peephole.ML \
   1.104 +  Tools/Nitpick/nitpick_rep.ML \
   1.105 +  Tools/Nitpick/nitpick_scope.ML \
   1.106 +  Tools/Nitpick/nitpick_tests.ML \
   1.107 +  Tools/Nitpick/nitpick_util.ML \
   1.108    Tools/inductive_codegen.ML \
   1.109    Tools/inductive.ML \
   1.110    Tools/inductive_realizer.ML \
   1.111 @@ -324,21 +354,17 @@
   1.112  
   1.113  $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/SetsAndFunctions.thy		\
   1.114    Library/Abstract_Rat.thy Library/BigO.thy Library/ContNotDenum.thy	\
   1.115 -  Library/Efficient_Nat.thy Library/Euclidean_Space.thy			\
   1.116 -  Library/Sum_Of_Squares.thy Library/Sum_Of_Squares/sos_wrapper.ML	\
   1.117 +  Library/Efficient_Nat.thy Library/Sum_Of_Squares.thy			\
   1.118 +  Library/Sum_Of_Squares/sos_wrapper.ML					\
   1.119    Library/Sum_Of_Squares/sum_of_squares.ML Library/Fset.thy		\
   1.120 -  Library/Convex_Euclidean_Space.thy Library/Glbs.thy			\
   1.121 -  Library/normarith.ML Library/Executable_Set.thy			\
   1.122 +  Library/Glbs.thy Library/normarith.ML Library/Executable_Set.thy	\
   1.123    Library/Infinite_Set.thy Library/FuncSet.thy				\
   1.124 -  Library/Permutations.thy Library/Determinants.thy Library/Bit.thy	\
   1.125 -  Library/Topology_Euclidean_Space.thy					\
   1.126 -  Library/Finite_Cartesian_Product.thy Library/FrechetDeriv.thy		\
   1.127 +  Library/Permutations.thy Library/Bit.thy Library/FrechetDeriv.thy	\
   1.128    Library/Fraction_Field.thy Library/Fundamental_Theorem_Algebra.thy	\
   1.129    Library/Inner_Product.thy Library/Kleene_Algebra.thy			\
   1.130 -  Library/Lattice_Syntax.thy			\
   1.131 -  Library/Library.thy Library/List_Prefix.thy Library/List_Set.thy	\
   1.132 -  Library/State_Monad.thy Library/Nat_Int_Bij.thy Library/Multiset.thy	\
   1.133 -  Library/Permutation.thy	\
   1.134 +  Library/Lattice_Syntax.thy Library/Library.thy			\
   1.135 +  Library/List_Prefix.thy Library/List_Set.thy Library/State_Monad.thy	\
   1.136 +  Library/Nat_Int_Bij.thy Library/Multiset.thy Library/Permutation.thy	\
   1.137    Library/Quotient.thy Library/Quicksort.thy Library/Nat_Infinity.thy	\
   1.138    Library/Word.thy Library/README.html Library/Continuity.thy		\
   1.139    Library/Order_Relation.thy Library/Nested_Environment.thy		\
   1.140 @@ -360,7 +386,7 @@
   1.141    Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML		\
   1.142    $(SRC)/HOL/Tools/float_arith.ML Library/positivstellensatz.ML		\
   1.143    Library/reify_data.ML Library/reflection.ML Library/LaTeXsugar.thy	\
   1.144 -  Library/OptionalSugar.thy
   1.145 +  Library/OptionalSugar.thy Library/SML_Quickcheck.thy
   1.146  	@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
   1.147  
   1.148  
   1.149 @@ -570,6 +596,21 @@
   1.150  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Metis_Examples
   1.151  
   1.152  
   1.153 +## HOL-Nitpick_Examples
   1.154 +
   1.155 +HOL-Nitpick_Examples: HOL $(LOG)/HOL-Nitpick_Examples.gz
   1.156 +
   1.157 +$(LOG)/HOL-Nitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML \
   1.158 +  Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy \
   1.159 +  Nitpick_Examples/Induct_Nits.thy Nitpick_Examples/Manual_Nits.thy \
   1.160 +  Nitpick_Examples/Mini_Nits.thy Nitpick_Examples/Mono_Nits.thy \
   1.161 +  Nitpick_Examples/Nitpick_Examples.thy Nitpick_Examples/Pattern_Nits.thy \
   1.162 +  Nitpick_Examples/Record_Nits.thy Nitpick_Examples/Refute_Nits.thy \
   1.163 +  Nitpick_Examples/Special_Nits.thy Nitpick_Examples/Tests_Nits.thy \
   1.164 +  Nitpick_Examples/Typedef_Nits.thy
   1.165 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Nitpick_Examples
   1.166 +
   1.167 +
   1.168  ## HOL-Algebra
   1.169  
   1.170  HOL-Algebra: HOL $(LOG)/HOL-Algebra.gz
   1.171 @@ -1006,6 +1047,19 @@
   1.172  	@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Memory
   1.173  
   1.174  
   1.175 +## HOL-Multivariate_Analysis
   1.176 +
   1.177 +HOL-Multivariate_Analysis: HOL $(OUT)/HOL-Multivariate_Analysis
   1.178 +
   1.179 +$(OUT)/HOL-Multivariate_Analysis: $(OUT)/HOL Multivariate_Analysis/ROOT.ML \
   1.180 +  Multivariate_Analysis/Multivariate_Analysis.thy \
   1.181 +  Multivariate_Analysis/Determinants.thy \
   1.182 +  Multivariate_Analysis/Finite_Cartesian_Product.thy \
   1.183 +  Multivariate_Analysis/Euclidean_Space.thy \
   1.184 +  Multivariate_Analysis/Topology_Euclidean_Space.thy \
   1.185 +  Multivariate_Analysis/Convex_Euclidean_Space.thy
   1.186 +	@cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Multivariate_Analysis
   1.187 +
   1.188  ## HOL-Nominal
   1.189  
   1.190  HOL-Nominal: HOL $(OUT)/HOL-Nominal
   1.191 @@ -1043,6 +1097,7 @@
   1.192    Nominal/Examples/Lam_Funs.thy \
   1.193    Nominal/Examples/Lambda_mu.thy \
   1.194    Nominal/Examples/LocalWeakening.thy \
   1.195 +  Nominal/Examples/Pattern.thy \
   1.196    Nominal/Examples/ROOT.ML \
   1.197    Nominal/Examples/SN.thy \
   1.198    Nominal/Examples/SOS.thy \
   1.199 @@ -1315,6 +1370,7 @@
   1.200  		$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Modelcheck.gz		\
   1.201  		$(LOG)/HOL-Lambda.gz $(LOG)/HOL-Bali.gz			\
   1.202  		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz		\
   1.203 +		$(OUT)/HOL-Multivariate_Analysis			\
   1.204  		$(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-IOA.gz	\
   1.205  		$(LOG)/HOL-Lattice $(LOG)/HOL-Matrix			\
   1.206  		$(LOG)/HOL-Hahn_Banach.gz $(LOG)/HOL-SET_Protocol.gz	\
   1.207 @@ -1322,7 +1378,7 @@
   1.208  		$(LOG)/TLA-Memory.gz $(LOG)/HOL-Library.gz		\
   1.209  		$(LOG)/HOL-Unix.gz $(OUT)/HOL-Word $(LOG)/HOL-Word.gz	\
   1.210  		$(LOG)/HOL-Word-Examples.gz $(OUT)/HOL-NSA		\
   1.211 -		$(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz            \
   1.212 -                $(LOG)/HOL-Mirabelle.gz $(LOG)/HOL-SMT.gz               \
   1.213 -                $(LOG)/HOL-SMT-Examples.gz
   1.214 +		$(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz		\
   1.215 +		$(LOG)/HOL-Mirabelle.gz $(OUT)/HOL-SMT			\
   1.216 +		$(LOG)/HOL-SMT.gz $(LOG)/HOL-SMT-Examples.gz
   1.217