--- a/src/HOL/IsaMakefile Tue Jun 05 15:17:02 2007 +0200
+++ b/src/HOL/IsaMakefile Tue Jun 05 16:26:04 2007 +0200
@@ -85,23 +85,28 @@
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 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/Presburger/cooper_dec.ML \
- Tools/Presburger/cooper_proof.ML Tools/Presburger/presburger.ML \
- Tools/Presburger/qelim.ML Tools/Presburger/reflected_cooper.ML \
+ 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/Groebner_Basis/groebner.ML Tools/Groebner_Basis/misc.ML \
+ Tools/Groebner_Basis/normalizer.ML \
+ Tools/Groebner_Basis/normalizer_data.ML \
+ Tools/Presburger/cooper_dec.ML Tools/Presburger/cooper_proof.ML \
+ Tools/Presburger/presburger.ML Tools/Presburger/qelim.ML \
+ Tools/Presburger/reflected_cooper.ML \
Tools/Presburger/reflected_presburger.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/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 \