added HOL-Base image
authorhaftmann
Fri Jan 16 08:29:11 2009 +0100 (2009-01-16)
changeset 29505c6d2d23909d1
parent 29504 4c3441f2f619
child 29508 b0e01a48867c
child 29509 1ff0f3f08a7b
added HOL-Base image
src/HOL/HOL.thy
src/HOL/IsaMakefile
src/HOL/base.ML
     1.1 --- a/src/HOL/HOL.thy	Fri Jan 16 08:28:53 2009 +0100
     1.2 +++ b/src/HOL/HOL.thy	Fri Jan 16 08:29:11 2009 +0100
     1.3 @@ -35,7 +35,7 @@
     1.4    "~~/src/Tools/code/code_ml.ML"
     1.5    "~~/src/Tools/code/code_haskell.ML"
     1.6    "~~/src/Tools/nbe.ML"
     1.7 -  ("~~/src/HOL/Tools/recfun_codegen.ML")
     1.8 +  ("Tools/recfun_codegen.ML")
     1.9  begin
    1.10  
    1.11  subsection {* Primitive logic *}
    1.12 @@ -1690,7 +1690,7 @@
    1.13  
    1.14  text {* Module setup *}
    1.15  
    1.16 -use "~~/src/HOL/Tools/recfun_codegen.ML"
    1.17 +use "Tools/recfun_codegen.ML"
    1.18  
    1.19  setup {*
    1.20    Code_ML.setup
     2.1 --- a/src/HOL/IsaMakefile	Fri Jan 16 08:28:53 2009 +0100
     2.2 +++ b/src/HOL/IsaMakefile	Fri Jan 16 08:29:11 2009 +0100
     2.3 @@ -6,7 +6,7 @@
     2.4  
     2.5  default: HOL
     2.6  generate: HOL-Generate-HOL HOL-Generate-HOLLight
     2.7 -images: HOL-Plain HOL-Main HOL HOL-Algebra HOL-Nominal HOL-NSA HOL-Word TLA HOL4
     2.8 +images: HOL HOL-Base HOL-Plain HOL-Main HOL-Algebra HOL-Nominal HOL-NSA HOL-Word TLA HOL4
     2.9  
    2.10  #Note: keep targets sorted (except for HOL-Library and HOL-ex)
    2.11  test: \
    2.12 @@ -66,6 +66,8 @@
    2.13  
    2.14  HOL: Pure $(OUT)/HOL
    2.15  
    2.16 +HOL-Base: Pure $(OUT)/HOL-Base
    2.17 +
    2.18  HOL-Plain: Pure $(OUT)/HOL-Plain
    2.19  
    2.20  HOL-Main: Pure $(OUT)/HOL-Main
    2.21 @@ -75,15 +77,50 @@
    2.22  
    2.23  $(OUT)/Pure: Pure
    2.24  
    2.25 -PLAIN_DEPENDENCIES = $(OUT)/Pure \
    2.26 +BASE_DEPENDENCIES = $(OUT)/Pure \
    2.27    Code_Setup.thy \
    2.28 +  HOL.thy \
    2.29 +  Tools/hologic.ML \
    2.30 +  Tools/recfun_codegen.ML \
    2.31 +  Tools/simpdata.ML \
    2.32 +  $(SRC)/Tools/atomize_elim.ML \
    2.33 +  $(SRC)/Tools/code/code_funcgr.ML \
    2.34 +  $(SRC)/Tools/code/code_funcgr.ML \
    2.35 +  $(SRC)/Tools/code/code_name.ML \
    2.36 +  $(SRC)/Tools/code/code_printer.ML \
    2.37 +  $(SRC)/Tools/code/code_target.ML \
    2.38 +  $(SRC)/Tools/code/code_ml.ML \
    2.39 +  $(SRC)/Tools/code/code_haskell.ML \
    2.40 +  $(SRC)/Tools/code/code_thingol.ML \
    2.41 +  $(SRC)/Tools/induct.ML \
    2.42 +  $(SRC)/Tools/induct_tacs.ML \
    2.43 +  $(SRC)/Tools/IsaPlanner/isand.ML \
    2.44 +  $(SRC)/Tools/IsaPlanner/rw_inst.ML \
    2.45 +  $(SRC)/Tools/IsaPlanner/rw_tools.ML \
    2.46 +  $(SRC)/Tools/IsaPlanner/zipper.ML \
    2.47 +  $(SRC)/Tools/nbe.ML \
    2.48 +  $(SRC)/Tools/random_word.ML \
    2.49 +  $(SRC)/Tools/value.ML \
    2.50 +  $(SRC)/Provers/blast.ML \
    2.51 +  $(SRC)/Provers/clasimp.ML \
    2.52 +  $(SRC)/Provers/classical.ML \
    2.53 +  $(SRC)/Provers/coherent.ML \
    2.54 +  $(SRC)/Provers/eqsubst.ML \
    2.55 +  $(SRC)/Provers/hypsubst.ML \
    2.56 +  $(SRC)/Provers/project_rule.ML \
    2.57 +  $(SRC)/Provers/quantifier1.ML \
    2.58 +  $(SRC)/Provers/splitter.ML \
    2.59 +
    2.60 +$(OUT)/HOL-Base: base.ML $(BASE_DEPENDENCIES)
    2.61 +	@$(ISABELLE_TOOL) usedir -b -f base.ML -g true $(OUT)/Pure HOL-Base
    2.62 +
    2.63 +PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES)\
    2.64    Datatype.thy \
    2.65    Divides.thy \
    2.66    Extraction.thy \
    2.67    Finite_Set.thy \
    2.68    Fun.thy \
    2.69    FunDef.thy \
    2.70 -  HOL.thy \
    2.71    Inductive.thy \
    2.72    Lattices.thy \
    2.73    Nat.thy \
    2.74 @@ -131,7 +168,6 @@
    2.75    Tools/function_package/size.ML \
    2.76    Tools/function_package/sum_tree.ML \
    2.77    Tools/function_package/termination.ML \
    2.78 -  Tools/hologic.ML \
    2.79    Tools/inductive_codegen.ML \
    2.80    Tools/inductive_package.ML \
    2.81    Tools/inductive_realizer.ML \
    2.82 @@ -140,14 +176,12 @@
    2.83    Tools/old_primrec_package.ML \
    2.84    Tools/primrec_package.ML \
    2.85    Tools/prop_logic.ML \
    2.86 -  Tools/recfun_codegen.ML \
    2.87    Tools/record_package.ML \
    2.88    Tools/refute.ML \
    2.89    Tools/refute_isar.ML \
    2.90    Tools/rewrite_hol_proof.ML \
    2.91    Tools/sat_funcs.ML \
    2.92    Tools/sat_solver.ML \
    2.93 -  Tools/simpdata.ML \
    2.94    Tools/split_rule.ML \
    2.95    Tools/typecopy_package.ML \
    2.96    Tools/typedef_codegen.ML \
    2.97 @@ -159,35 +193,8 @@
    2.98    $(SRC)/Provers/Arith/cancel_div_mod.ML \
    2.99    $(SRC)/Provers/Arith/cancel_sums.ML \
   2.100    $(SRC)/Provers/Arith/fast_lin_arith.ML \
   2.101 -  $(SRC)/Provers/blast.ML \
   2.102 -  $(SRC)/Provers/clasimp.ML \
   2.103 -  $(SRC)/Provers/classical.ML \
   2.104 -  $(SRC)/Provers/coherent.ML \
   2.105 -  $(SRC)/Provers/eqsubst.ML \
   2.106 -  $(SRC)/Provers/hypsubst.ML \
   2.107    $(SRC)/Provers/order.ML \
   2.108 -  $(SRC)/Provers/project_rule.ML \
   2.109 -  $(SRC)/Provers/quantifier1.ML \
   2.110 -  $(SRC)/Provers/splitter.ML \
   2.111    $(SRC)/Provers/trancl.ML \
   2.112 -  $(SRC)/Tools/IsaPlanner/isand.ML \
   2.113 -  $(SRC)/Tools/IsaPlanner/rw_inst.ML \
   2.114 -  $(SRC)/Tools/IsaPlanner/rw_tools.ML \
   2.115 -  $(SRC)/Tools/IsaPlanner/zipper.ML \
   2.116 -  $(SRC)/Tools/atomize_elim.ML \
   2.117 -  $(SRC)/Tools/code/code_funcgr.ML \
   2.118 -  $(SRC)/Tools/code/code_funcgr.ML \
   2.119 -  $(SRC)/Tools/code/code_name.ML \
   2.120 -  $(SRC)/Tools/code/code_printer.ML \
   2.121 -  $(SRC)/Tools/code/code_target.ML \
   2.122 -  $(SRC)/Tools/code/code_ml.ML \
   2.123 -  $(SRC)/Tools/code/code_haskell.ML \
   2.124 -  $(SRC)/Tools/code/code_thingol.ML \
   2.125 -  $(SRC)/Tools/induct.ML \
   2.126 -  $(SRC)/Tools/induct_tacs.ML \
   2.127 -  $(SRC)/Tools/value.ML \
   2.128 -  $(SRC)/Tools/nbe.ML \
   2.129 -  $(SRC)/Tools/random_word.ML \
   2.130    $(SRC)/Tools/rat.ML
   2.131  
   2.132  $(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES)
   2.133 @@ -280,7 +287,6 @@
   2.134    GCD.thy \
   2.135    Order_Relation.thy \
   2.136    Parity.thy \
   2.137 -  Univ_Poly.thy \
   2.138    Lubs.thy \
   2.139    Polynomial.thy \
   2.140    PReal.thy \
   2.141 @@ -327,7 +333,7 @@
   2.142    Library/Code_Char_chr.thy Library/Code_Integer.thy			\
   2.143    Library/Numeral_Type.thy			\
   2.144    Library/Boolean_Algebra.thy Library/Countable.thy	\
   2.145 -  Library/RBT.thy		\
   2.146 +  Library/RBT.thy	Library/Univ_Poly.thy	\
   2.147    Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML
   2.148  	@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
   2.149  
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/base.ML	Fri Jan 16 08:29:11 2009 +0100
     3.3 @@ -0,0 +1,2 @@
     3.4 +(*side-entry for HOL-Base*)
     3.5 +use_thy "Code_Setup";