# HG changeset patch
# User haftmann
# Date 1232090951 -3600
# Node ID c6d2d23909d1b2030d5a6622477030c083b56f07
# Parent  4c3441f2f61996a8233817cbbd472e853e862c29
added HOL-Base image

diff -r 4c3441f2f619 -r c6d2d23909d1 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Jan 16 08:28:53 2009 +0100
+++ b/src/HOL/HOL.thy	Fri Jan 16 08:29:11 2009 +0100
@@ -35,7 +35,7 @@
   "~~/src/Tools/code/code_ml.ML"
   "~~/src/Tools/code/code_haskell.ML"
   "~~/src/Tools/nbe.ML"
-  ("~~/src/HOL/Tools/recfun_codegen.ML")
+  ("Tools/recfun_codegen.ML")
 begin
 
 subsection {* Primitive logic *}
@@ -1690,7 +1690,7 @@
 
 text {* Module setup *}
 
-use "~~/src/HOL/Tools/recfun_codegen.ML"
+use "Tools/recfun_codegen.ML"
 
 setup {*
   Code_ML.setup
diff -r 4c3441f2f619 -r c6d2d23909d1 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Jan 16 08:28:53 2009 +0100
+++ b/src/HOL/IsaMakefile	Fri Jan 16 08:29:11 2009 +0100
@@ -6,7 +6,7 @@
 
 default: HOL
 generate: HOL-Generate-HOL HOL-Generate-HOLLight
-images: HOL-Plain HOL-Main HOL HOL-Algebra HOL-Nominal HOL-NSA HOL-Word TLA HOL4
+images: HOL HOL-Base HOL-Plain HOL-Main HOL-Algebra HOL-Nominal HOL-NSA HOL-Word TLA HOL4
 
 #Note: keep targets sorted (except for HOL-Library and HOL-ex)
 test: \
@@ -66,6 +66,8 @@
 
 HOL: Pure $(OUT)/HOL
 
+HOL-Base: Pure $(OUT)/HOL-Base
+
 HOL-Plain: Pure $(OUT)/HOL-Plain
 
 HOL-Main: Pure $(OUT)/HOL-Main
@@ -75,15 +77,50 @@
 
 $(OUT)/Pure: Pure
 
-PLAIN_DEPENDENCIES = $(OUT)/Pure \
+BASE_DEPENDENCIES = $(OUT)/Pure \
   Code_Setup.thy \
+  HOL.thy \
+  Tools/hologic.ML \
+  Tools/recfun_codegen.ML \
+  Tools/simpdata.ML \
+  $(SRC)/Tools/atomize_elim.ML \
+  $(SRC)/Tools/code/code_funcgr.ML \
+  $(SRC)/Tools/code/code_funcgr.ML \
+  $(SRC)/Tools/code/code_name.ML \
+  $(SRC)/Tools/code/code_printer.ML \
+  $(SRC)/Tools/code/code_target.ML \
+  $(SRC)/Tools/code/code_ml.ML \
+  $(SRC)/Tools/code/code_haskell.ML \
+  $(SRC)/Tools/code/code_thingol.ML \
+  $(SRC)/Tools/induct.ML \
+  $(SRC)/Tools/induct_tacs.ML \
+  $(SRC)/Tools/IsaPlanner/isand.ML \
+  $(SRC)/Tools/IsaPlanner/rw_inst.ML \
+  $(SRC)/Tools/IsaPlanner/rw_tools.ML \
+  $(SRC)/Tools/IsaPlanner/zipper.ML \
+  $(SRC)/Tools/nbe.ML \
+  $(SRC)/Tools/random_word.ML \
+  $(SRC)/Tools/value.ML \
+  $(SRC)/Provers/blast.ML \
+  $(SRC)/Provers/clasimp.ML \
+  $(SRC)/Provers/classical.ML \
+  $(SRC)/Provers/coherent.ML \
+  $(SRC)/Provers/eqsubst.ML \
+  $(SRC)/Provers/hypsubst.ML \
+  $(SRC)/Provers/project_rule.ML \
+  $(SRC)/Provers/quantifier1.ML \
+  $(SRC)/Provers/splitter.ML \
+
+$(OUT)/HOL-Base: base.ML $(BASE_DEPENDENCIES)
+	@$(ISABELLE_TOOL) usedir -b -f base.ML -g true $(OUT)/Pure HOL-Base
+
+PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES)\
   Datatype.thy \
   Divides.thy \
   Extraction.thy \
   Finite_Set.thy \
   Fun.thy \
   FunDef.thy \
-  HOL.thy \
   Inductive.thy \
   Lattices.thy \
   Nat.thy \
@@ -131,7 +168,6 @@
   Tools/function_package/size.ML \
   Tools/function_package/sum_tree.ML \
   Tools/function_package/termination.ML \
-  Tools/hologic.ML \
   Tools/inductive_codegen.ML \
   Tools/inductive_package.ML \
   Tools/inductive_realizer.ML \
@@ -140,14 +176,12 @@
   Tools/old_primrec_package.ML \
   Tools/primrec_package.ML \
   Tools/prop_logic.ML \
-  Tools/recfun_codegen.ML \
   Tools/record_package.ML \
   Tools/refute.ML \
   Tools/refute_isar.ML \
   Tools/rewrite_hol_proof.ML \
   Tools/sat_funcs.ML \
   Tools/sat_solver.ML \
-  Tools/simpdata.ML \
   Tools/split_rule.ML \
   Tools/typecopy_package.ML \
   Tools/typedef_codegen.ML \
@@ -159,35 +193,8 @@
   $(SRC)/Provers/Arith/cancel_div_mod.ML \
   $(SRC)/Provers/Arith/cancel_sums.ML \
   $(SRC)/Provers/Arith/fast_lin_arith.ML \
-  $(SRC)/Provers/blast.ML \
-  $(SRC)/Provers/clasimp.ML \
-  $(SRC)/Provers/classical.ML \
-  $(SRC)/Provers/coherent.ML \
-  $(SRC)/Provers/eqsubst.ML \
-  $(SRC)/Provers/hypsubst.ML \
   $(SRC)/Provers/order.ML \
-  $(SRC)/Provers/project_rule.ML \
-  $(SRC)/Provers/quantifier1.ML \
-  $(SRC)/Provers/splitter.ML \
   $(SRC)/Provers/trancl.ML \
-  $(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/code/code_funcgr.ML \
-  $(SRC)/Tools/code/code_funcgr.ML \
-  $(SRC)/Tools/code/code_name.ML \
-  $(SRC)/Tools/code/code_printer.ML \
-  $(SRC)/Tools/code/code_target.ML \
-  $(SRC)/Tools/code/code_ml.ML \
-  $(SRC)/Tools/code/code_haskell.ML \
-  $(SRC)/Tools/code/code_thingol.ML \
-  $(SRC)/Tools/induct.ML \
-  $(SRC)/Tools/induct_tacs.ML \
-  $(SRC)/Tools/value.ML \
-  $(SRC)/Tools/nbe.ML \
-  $(SRC)/Tools/random_word.ML \
   $(SRC)/Tools/rat.ML
 
 $(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES)
@@ -280,7 +287,6 @@
   GCD.thy \
   Order_Relation.thy \
   Parity.thy \
-  Univ_Poly.thy \
   Lubs.thy \
   Polynomial.thy \
   PReal.thy \
@@ -327,7 +333,7 @@
   Library/Code_Char_chr.thy Library/Code_Integer.thy			\
   Library/Numeral_Type.thy			\
   Library/Boolean_Algebra.thy Library/Countable.thy	\
-  Library/RBT.thy		\
+  Library/RBT.thy	Library/Univ_Poly.thy	\
   Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML
 	@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
 
diff -r 4c3441f2f619 -r c6d2d23909d1 src/HOL/base.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/base.ML	Fri Jan 16 08:29:11 2009 +0100
@@ -0,0 +1,2 @@
+(*side-entry for HOL-Base*)
+use_thy "Code_Setup";