--- a/src/HOL/IsaMakefile Thu Jun 21 15:42:06 2007 +0200
+++ b/src/HOL/IsaMakefile Thu Jun 21 15:42:07 2007 +0200
@@ -82,31 +82,32 @@
$(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML \
$(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML \
$(SRC)/Provers/trancl.ML $(SRC)/Tools/integer.ML \
- $(SRC)/Tools/rat.ML Tools/TFL/casesplit.ML \
- ATP_Linkup.thy Accessible_Part.thy Datatype.thy \
- Divides.thy Equiv_Relations.thy Extraction.thy Finite_Set.thy \
- FixedPoint.thy Fun.thy FunDef.thy HOL.thy Hilbert_Choice.thy \
- Inductive.thy IntArith.thy IntDef.thy IntDiv.thy Lattices.thy \
- List.thy Main.thy Map.thy Nat.ML Nat.thy NatBin.thy NatSimprocs.thy \
- Numeral.thy OrderedGroup.thy Orderings.thy Power.thy PreList.thy \
- Predicate.thy Presburger.thy Product_Type.thy ROOT.ML Recdef.thy \
+ $(SRC)/Tools/rat.ML Tools/TFL/casesplit.ML ATP_Linkup.thy \
+ Accessible_Part.thy Datatype.thy Dense_Linear_Order.thy Divides.thy \
+ Equiv_Relations.thy Extraction.thy Finite_Set.thy FixedPoint.thy \
+ Fun.thy FunDef.thy HOL.thy Hilbert_Choice.thy Inductive.thy \
+ IntArith.thy IntDef.thy IntDiv.thy Lattices.thy List.thy Main.thy \
+ Map.thy Nat.ML Nat.thy NatBin.thy NatSimprocs.thy Numeral.thy \
+ OrderedGroup.thy Orderings.thy Power.thy PreList.thy Predicate.thy \
+ Presburger.thy Product_Type.thy ROOT.ML Recdef.thy \
Record.thy Refute.thy Relation.thy Relation_Power.thy \
Ring_and_Field.thy SAT.thy Set.thy SetInterval.thy Sum_Type.thy \
Tools/ATP/reduce_axiomsN.ML Tools/ATP/watcher.ML \
+ Tools/Ferrante_Rackoff/ferrante_rackoff_data.ML \
+ Tools/Ferrante_Rackoff/ferrante_rackoff.ML \
Tools/Groebner_Basis/groebner.ML Tools/Groebner_Basis/misc.ML \
Tools/Groebner_Basis/normalizer.ML Groebner_Basis.thy \
Tools/Groebner_Basis/normalizer_data.ML \
Tools/Presburger/cooper.ML Tools/Presburger/presburger.ML \
- Tools/Presburger/qelim.ML Tools/Presburger/generated_cooper.ML \
- Tools/Presburger/cooper_data.ML Tools/TFL/dcterm.ML \
- Tools/TFL/post.ML Tools/TFL/rules.ML Tools/TFL/tfl.ML \
- Tools/TFL/thms.ML Tools/TFL/thry.ML Tools/TFL/usyntax.ML \
- Tools/TFL/utils.ML Tools/cnf_funcs.ML Tools/datatype_abs_proofs.ML \
- Tools/datatype_aux.ML Tools/datatype_case.ML \
- Tools/datatype_codegen.ML Tools/datatype_hooks.ML \
- Tools/datatype_package.ML Tools/datatype_prop.ML \
- Tools/datatype_realizer.ML Tools/datatype_rep_proofs.ML \
- Tools/function_package/auto_term.ML \
+ Tools/Presburger/generated_cooper.ML Tools/Presburger/cooper_data.ML \
+ Tools/TFL/dcterm.ML Tools/TFL/post.ML Tools/TFL/rules.ML \
+ Tools/TFL/tfl.ML Tools/TFL/thms.ML Tools/TFL/thry.ML \
+ Tools/TFL/usyntax.ML Tools/TFL/utils.ML Tools/cnf_funcs.ML \
+ Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
+ Tools/datatype_case.ML Tools/datatype_codegen.ML \
+ Tools/datatype_hooks.ML Tools/datatype_package.ML \
+ Tools/datatype_prop.ML Tools/datatype_realizer.ML \
+ Tools/datatype_rep_proofs.ML Tools/function_package/auto_term.ML \
Tools/function_package/context_tree.ML \
Tools/function_package/fundef_common.ML \
Tools/function_package/fundef_core.ML \
@@ -121,11 +122,12 @@
Tools/inductive_package.ML Tools/inductive_realizer.ML Tools/meson.ML \
Tools/metis_tools.ML Tools/numeral_syntax.ML \
Tools/old_inductive_package.ML Tools/polyhash.ML \
- Tools/primrec_package.ML Tools/prop_logic.ML Tools/recdef_package.ML \
- Tools/recfun_codegen.ML Tools/record_package.ML Tools/refute.ML \
- Tools/refute_isar.ML Tools/res_atp.ML Tools/res_atp_methods.ML \
- Tools/res_atp_provers.ML Tools/res_atpset.ML Tools/res_axioms.ML \
- Tools/res_clause.ML Tools/res_hol_clause.ML Tools/res_reconstruct.ML \
+ Tools/primrec_package.ML Tools/prop_logic.ML Tools/qelim.ML \
+ Tools/recdef_package.ML Tools/recfun_codegen.ML \
+ Tools/record_package.ML Tools/refute.ML Tools/refute_isar.ML \
+ Tools/res_atp.ML Tools/res_atp_methods.ML Tools/res_atp_provers.ML \
+ Tools/res_atpset.ML Tools/res_axioms.ML Tools/res_clause.ML \
+ Tools/res_hol_clause.ML Tools/res_reconstruct.ML \
Tools/rewrite_hol_proof.ML Tools/sat_funcs.ML Tools/sat_solver.ML \
Tools/specification_package.ML Tools/split_rule.ML \
Tools/string_syntax.ML Tools/typecopy_package.ML \
@@ -159,11 +161,10 @@
$(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML $(SRC)/Tools/float.ML \
Library/Zorn.thy \
- Real/ContNotDenum.thy Real/Ferrante_Rackoff.thy Real/float_arith.ML \
- Real/Float.thy Real/Lubs.thy Real/PReal.thy Real/RComplete.thy \
- Real/ROOT.ML Real/Rational.thy Real/Real.thy Real/RealDef.thy \
- Real/RealPow.thy Real/RealVector.thy Real/ferrante_rackoff_proof.ML \
- Real/ferrante_rackoff.ML Real/rat_arith.ML Real/real_arith.ML \
+ Real/ContNotDenum.thy Real/float_arith.ML Real/Float.thy \
+ Real/Lubs.thy Real/PReal.thy Real/RComplete.thy Real/ROOT.ML \
+ Real/Rational.thy Real/Real.thy Real/RealDef.thy Real/RealPow.thy \
+ Real/RealVector.thy Real/rat_arith.ML Real/real_arith.ML \
Hyperreal/StarDef.thy Hyperreal/StarClasses.thy \
Hyperreal/EvenOdd.thy Hyperreal/Fact.thy Hyperreal/HLog.thy \
Hyperreal/Filter.thy Hyperreal/HSeries.thy Hyperreal/transfer.ML \
@@ -190,7 +191,6 @@
$(LOG)/HOL-Complex-ex.gz: $(OUT)/HOL-Complex Library/Primes.thy \
Complex/ex/ROOT.ML Complex/ex/document/root.tex \
Complex/ex/BigO_Complex.thy Complex/ex/BinEx.thy \
- Complex/ex/Ferrante_Rackoff_Ex.thy \
Complex/ex/NSPrimes.thy Complex/ex/Sqrt.thy Complex/ex/Sqrt_Script.thy \
Complex/ex/MIR.thy Complex/ex/mirtac.ML Complex/ex/mireif.ML \
Complex/ex/ReflectedFerrack.thy Complex/ex/linreif.ML Complex/ex/linrtac.ML
@@ -400,7 +400,7 @@
MetisExamples/Abstraction.thy MetisExamples/BigO.thy MetisExamples/BT.thy \
MetisExamples/Message.thy MetisExamples/Tarski.thy MetisExamples/TransClosure.thy \
MetisExamples/set.thy
- @$(ISATOOL) usedir -g true $(OUT)/HOL MetisExamples
+ @$(ISATOOL) usedir $(OUT)/HOL MetisExamples
## HOL-Algebra
@@ -649,7 +649,7 @@
$(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy \
ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy \
ex/BT.thy ex/BinEx.thy ex/CTL.thy \
- ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy \
+ ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy ex/Dense_Linear_Order_Ex.thy \
ex/Eval_Examples.thy ex/Groebner_Examples.thy ex/Random.thy \
ex/Codegenerator.thy ex/Codegenerator_Rat.thy \
ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy \