separate HOL-Main image
authorhaftmann
Mon Sep 29 12:31:58 2008 +0200 (2008-09-29)
changeset 28401d5f39173444c
parent 28400 89904cfd41c3
child 28402 09e4aa3ddc25
separate HOL-Main image
src/HOL/IsaMakefile
src/HOL/main.ML
     1.1 --- a/src/HOL/IsaMakefile	Mon Sep 29 12:31:57 2008 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Sep 29 12:31:58 2008 +0200
     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 HOL-Algebra HOL-Nominal HOL-NSA HOL-Word TLA HOL4
     1.8 +images: HOL-Plain HOL-Main HOL 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-Plain: Pure $(OUT)/HOL-Plain
    1.15  
    1.16 +HOL-Main: Pure $(OUT)/HOL-Main
    1.17 +
    1.18  Pure:
    1.19  	@cd $(SRC)/Pure; $(ISATOOL) make Pure
    1.20  
    1.21 @@ -182,38 +184,18 @@
    1.22  $(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES)
    1.23  	@$(ISATOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
    1.24  
    1.25 -$(OUT)/HOL: ROOT.ML $(PLAIN_DEPENDENCIES) \
    1.26 +MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
    1.27    Arith_Tools.thy \
    1.28    ATP_Linkup.thy \
    1.29    Code_Eval.thy \
    1.30 -  Complex/Complex_Main.thy \
    1.31 -  Complex/Complex.thy \
    1.32 -  Complex/Fundamental_Theorem_Algebra.thy \
    1.33    Equiv_Relations.thy \
    1.34    Groebner_Basis.thy \
    1.35    Hilbert_Choice.thy \
    1.36 -  Hyperreal/Deriv.thy \
    1.37 -  Hyperreal/Fact.thy \
    1.38 -  Hyperreal/Integration.thy \
    1.39 -  Hyperreal/Lim.thy \
    1.40 -  Hyperreal/Ln.thy \
    1.41 -  Hyperreal/Log.thy \
    1.42 -  Hyperreal/MacLaurin.thy \
    1.43 -  Hyperreal/NthRoot.thy \
    1.44 -  Hyperreal/SEQ.thy \
    1.45 -  Hyperreal/Series.thy \
    1.46 -  Hyperreal/Taylor.thy \
    1.47 -  Hyperreal/Transcendental.thy \
    1.48    int_arith1.ML \
    1.49    IntDiv.thy \
    1.50    int_factor_simprocs.ML \
    1.51    Int.thy \
    1.52 -  Library/Dense_Linear_Order.thy \
    1.53 -  Library/GCD.thy \
    1.54 -  Library/Order_Relation.thy \
    1.55 -  Library/Parity.thy \
    1.56    Library/RType.thy \
    1.57 -  Library/Univ_Poly.thy \
    1.58    List.thy \
    1.59    Main.thy \
    1.60    Map.thy \
    1.61 @@ -221,17 +203,6 @@
    1.62    Nat_Int_Bij.thy \
    1.63    nat_simprocs.ML \
    1.64    Presburger.thy \
    1.65 -  Real/ContNotDenum.thy \
    1.66 -  Real/Lubs.thy \
    1.67 -  Real/PReal.thy \
    1.68 -  Real/rat_arith.ML \
    1.69 -  Real/Rational.thy \
    1.70 -  Real/RComplete.thy \
    1.71 -  Real/real_arith.ML \
    1.72 -  Real/RealDef.thy \
    1.73 -  Real/RealPow.thy \
    1.74 -  Real/Real.thy \
    1.75 -  Real/RealVector.thy \
    1.76    Recdef.thy \
    1.77    Relation_Power.thy \
    1.78    SetInterval.thy \
    1.79 @@ -252,11 +223,7 @@
    1.80    Tools/polyhash.ML \
    1.81    Tools/Qelim/cooper_data.ML \
    1.82    Tools/Qelim/cooper.ML \
    1.83 -  Tools/Qelim/ferrante_rackoff_data.ML \
    1.84 -  Tools/Qelim/ferrante_rackoff.ML \
    1.85    Tools/Qelim/generated_cooper.ML \
    1.86 -  Tools/Qelim/langford_data.ML \
    1.87 -  Tools/Qelim/langford.ML \
    1.88    Tools/Qelim/presburger.ML \
    1.89    Tools/Qelim/qelim.ML \
    1.90    Tools/recdef_package.ML \
    1.91 @@ -279,6 +246,46 @@
    1.92    Tools/TFL/usyntax.ML \
    1.93    Tools/TFL/utils.ML \
    1.94    Tools/watcher.ML
    1.95 +
    1.96 +$(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES)
    1.97 +	@$(ISATOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
    1.98 +
    1.99 +$(OUT)/HOL: ROOT.ML $(MAIN_DEPENDENCIES) \
   1.100 +  Complex/Complex_Main.thy \
   1.101 +  Complex/Complex.thy \
   1.102 +  Complex/Fundamental_Theorem_Algebra.thy \
   1.103 +  Hyperreal/Deriv.thy \
   1.104 +  Hyperreal/Fact.thy \
   1.105 +  Hyperreal/Integration.thy \
   1.106 +  Hyperreal/Lim.thy \
   1.107 +  Hyperreal/Ln.thy \
   1.108 +  Hyperreal/Log.thy \
   1.109 +  Hyperreal/MacLaurin.thy \
   1.110 +  Hyperreal/NthRoot.thy \
   1.111 +  Hyperreal/SEQ.thy \
   1.112 +  Hyperreal/Series.thy \
   1.113 +  Hyperreal/Taylor.thy \
   1.114 +  Hyperreal/Transcendental.thy \
   1.115 +  Library/Dense_Linear_Order.thy \
   1.116 +  Library/GCD.thy \
   1.117 +  Library/Order_Relation.thy \
   1.118 +  Library/Parity.thy \
   1.119 +  Library/Univ_Poly.thy \
   1.120 +  Real/ContNotDenum.thy \
   1.121 +  Real/Lubs.thy \
   1.122 +  Real/PReal.thy \
   1.123 +  Real/rat_arith.ML \
   1.124 +  Real/Rational.thy \
   1.125 +  Real/RComplete.thy \
   1.126 +  Real/real_arith.ML \
   1.127 +  Real/RealDef.thy \
   1.128 +  Real/RealPow.thy \
   1.129 +  Real/Real.thy \
   1.130 +  Real/RealVector.thy \
   1.131 +  Tools/Qelim/ferrante_rackoff_data.ML \
   1.132 +  Tools/Qelim/ferrante_rackoff.ML \
   1.133 +  Tools/Qelim/langford_data.ML \
   1.134 +  Tools/Qelim/langford.ML
   1.135  	@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL
   1.136  
   1.137  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/main.ML	Mon Sep 29 12:31:58 2008 +0200
     2.3 @@ -0,0 +1,7 @@
     2.4 +(*  Title:      HOL/main.ML
     2.5 +    ID:         $Id$
     2.6 + 
     2.7 +Classical Higher-order Logic -- only "Main".
     2.8 +*)
     2.9 +
    2.10 +use_thy "Main";