src/HOL/IsaMakefile
changeset 29505 c6d2d23909d1
parent 29463 6660f9019673
child 29523 f83dcdcee6b3
     1.1 --- a/src/HOL/IsaMakefile	Fri Jan 16 08:28:53 2009 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Jan 16 08:29:11 2009 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  default: HOL
     1.6  generate: HOL-Generate-HOL HOL-Generate-HOLLight
     1.7 -images: HOL-Plain HOL-Main HOL HOL-Algebra HOL-Nominal HOL-NSA HOL-Word TLA HOL4
     1.8 +images: HOL HOL-Base HOL-Plain HOL-Main HOL-Algebra HOL-Nominal HOL-NSA HOL-Word TLA HOL4
     1.9  
    1.10  #Note: keep targets sorted (except for HOL-Library and HOL-ex)
    1.11  test: \
    1.12 @@ -66,6 +66,8 @@
    1.13  
    1.14  HOL: Pure $(OUT)/HOL
    1.15  
    1.16 +HOL-Base: Pure $(OUT)/HOL-Base
    1.17 +
    1.18  HOL-Plain: Pure $(OUT)/HOL-Plain
    1.19  
    1.20  HOL-Main: Pure $(OUT)/HOL-Main
    1.21 @@ -75,15 +77,50 @@
    1.22  
    1.23  $(OUT)/Pure: Pure
    1.24  
    1.25 -PLAIN_DEPENDENCIES = $(OUT)/Pure \
    1.26 +BASE_DEPENDENCIES = $(OUT)/Pure \
    1.27    Code_Setup.thy \
    1.28 +  HOL.thy \
    1.29 +  Tools/hologic.ML \
    1.30 +  Tools/recfun_codegen.ML \
    1.31 +  Tools/simpdata.ML \
    1.32 +  $(SRC)/Tools/atomize_elim.ML \
    1.33 +  $(SRC)/Tools/code/code_funcgr.ML \
    1.34 +  $(SRC)/Tools/code/code_funcgr.ML \
    1.35 +  $(SRC)/Tools/code/code_name.ML \
    1.36 +  $(SRC)/Tools/code/code_printer.ML \
    1.37 +  $(SRC)/Tools/code/code_target.ML \
    1.38 +  $(SRC)/Tools/code/code_ml.ML \
    1.39 +  $(SRC)/Tools/code/code_haskell.ML \
    1.40 +  $(SRC)/Tools/code/code_thingol.ML \
    1.41 +  $(SRC)/Tools/induct.ML \
    1.42 +  $(SRC)/Tools/induct_tacs.ML \
    1.43 +  $(SRC)/Tools/IsaPlanner/isand.ML \
    1.44 +  $(SRC)/Tools/IsaPlanner/rw_inst.ML \
    1.45 +  $(SRC)/Tools/IsaPlanner/rw_tools.ML \
    1.46 +  $(SRC)/Tools/IsaPlanner/zipper.ML \
    1.47 +  $(SRC)/Tools/nbe.ML \
    1.48 +  $(SRC)/Tools/random_word.ML \
    1.49 +  $(SRC)/Tools/value.ML \
    1.50 +  $(SRC)/Provers/blast.ML \
    1.51 +  $(SRC)/Provers/clasimp.ML \
    1.52 +  $(SRC)/Provers/classical.ML \
    1.53 +  $(SRC)/Provers/coherent.ML \
    1.54 +  $(SRC)/Provers/eqsubst.ML \
    1.55 +  $(SRC)/Provers/hypsubst.ML \
    1.56 +  $(SRC)/Provers/project_rule.ML \
    1.57 +  $(SRC)/Provers/quantifier1.ML \
    1.58 +  $(SRC)/Provers/splitter.ML \
    1.59 +
    1.60 +$(OUT)/HOL-Base: base.ML $(BASE_DEPENDENCIES)
    1.61 +	@$(ISABELLE_TOOL) usedir -b -f base.ML -g true $(OUT)/Pure HOL-Base
    1.62 +
    1.63 +PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES)\
    1.64    Datatype.thy \
    1.65    Divides.thy \
    1.66    Extraction.thy \
    1.67    Finite_Set.thy \
    1.68    Fun.thy \
    1.69    FunDef.thy \
    1.70 -  HOL.thy \
    1.71    Inductive.thy \
    1.72    Lattices.thy \
    1.73    Nat.thy \
    1.74 @@ -131,7 +168,6 @@
    1.75    Tools/function_package/size.ML \
    1.76    Tools/function_package/sum_tree.ML \
    1.77    Tools/function_package/termination.ML \
    1.78 -  Tools/hologic.ML \
    1.79    Tools/inductive_codegen.ML \
    1.80    Tools/inductive_package.ML \
    1.81    Tools/inductive_realizer.ML \
    1.82 @@ -140,14 +176,12 @@
    1.83    Tools/old_primrec_package.ML \
    1.84    Tools/primrec_package.ML \
    1.85    Tools/prop_logic.ML \
    1.86 -  Tools/recfun_codegen.ML \
    1.87    Tools/record_package.ML \
    1.88    Tools/refute.ML \
    1.89    Tools/refute_isar.ML \
    1.90    Tools/rewrite_hol_proof.ML \
    1.91    Tools/sat_funcs.ML \
    1.92    Tools/sat_solver.ML \
    1.93 -  Tools/simpdata.ML \
    1.94    Tools/split_rule.ML \
    1.95    Tools/typecopy_package.ML \
    1.96    Tools/typedef_codegen.ML \
    1.97 @@ -159,35 +193,8 @@
    1.98    $(SRC)/Provers/Arith/cancel_div_mod.ML \
    1.99    $(SRC)/Provers/Arith/cancel_sums.ML \
   1.100    $(SRC)/Provers/Arith/fast_lin_arith.ML \
   1.101 -  $(SRC)/Provers/blast.ML \
   1.102 -  $(SRC)/Provers/clasimp.ML \
   1.103 -  $(SRC)/Provers/classical.ML \
   1.104 -  $(SRC)/Provers/coherent.ML \
   1.105 -  $(SRC)/Provers/eqsubst.ML \
   1.106 -  $(SRC)/Provers/hypsubst.ML \
   1.107    $(SRC)/Provers/order.ML \
   1.108 -  $(SRC)/Provers/project_rule.ML \
   1.109 -  $(SRC)/Provers/quantifier1.ML \
   1.110 -  $(SRC)/Provers/splitter.ML \
   1.111    $(SRC)/Provers/trancl.ML \
   1.112 -  $(SRC)/Tools/IsaPlanner/isand.ML \
   1.113 -  $(SRC)/Tools/IsaPlanner/rw_inst.ML \
   1.114 -  $(SRC)/Tools/IsaPlanner/rw_tools.ML \
   1.115 -  $(SRC)/Tools/IsaPlanner/zipper.ML \
   1.116 -  $(SRC)/Tools/atomize_elim.ML \
   1.117 -  $(SRC)/Tools/code/code_funcgr.ML \
   1.118 -  $(SRC)/Tools/code/code_funcgr.ML \
   1.119 -  $(SRC)/Tools/code/code_name.ML \
   1.120 -  $(SRC)/Tools/code/code_printer.ML \
   1.121 -  $(SRC)/Tools/code/code_target.ML \
   1.122 -  $(SRC)/Tools/code/code_ml.ML \
   1.123 -  $(SRC)/Tools/code/code_haskell.ML \
   1.124 -  $(SRC)/Tools/code/code_thingol.ML \
   1.125 -  $(SRC)/Tools/induct.ML \
   1.126 -  $(SRC)/Tools/induct_tacs.ML \
   1.127 -  $(SRC)/Tools/value.ML \
   1.128 -  $(SRC)/Tools/nbe.ML \
   1.129 -  $(SRC)/Tools/random_word.ML \
   1.130    $(SRC)/Tools/rat.ML
   1.131  
   1.132  $(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES)
   1.133 @@ -280,7 +287,6 @@
   1.134    GCD.thy \
   1.135    Order_Relation.thy \
   1.136    Parity.thy \
   1.137 -  Univ_Poly.thy \
   1.138    Lubs.thy \
   1.139    Polynomial.thy \
   1.140    PReal.thy \
   1.141 @@ -327,7 +333,7 @@
   1.142    Library/Code_Char_chr.thy Library/Code_Integer.thy			\
   1.143    Library/Numeral_Type.thy			\
   1.144    Library/Boolean_Algebra.thy Library/Countable.thy	\
   1.145 -  Library/RBT.thy		\
   1.146 +  Library/RBT.thy	Library/Univ_Poly.thy	\
   1.147    Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML
   1.148  	@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
   1.149