--- a/src/HOL/IsaMakefile Thu May 31 18:16:51 2007 +0200
+++ b/src/HOL/IsaMakefile Thu May 31 18:16:52 2007 +0200
@@ -82,26 +82,23 @@
$(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML \
$(SRC)/Provers/trancl.ML $(SRC)/Pure/General/int.ML \
$(SRC)/Pure/General/rat.ML Tools/TFL/casesplit.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 ATP_Linkup.thy \
- Accessible_Part.thy Code_Generator.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 \
- Integ/IntArith.thy Integ/IntDef.thy Integ/IntDiv.thy Integ/NatBin.thy \
- Integ/NatSimprocs.thy Integ/Numeral.thy Integ/int_arith1.ML \
- Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML Lattices.thy \
- List.thy Main.thy Map.thy Nat.ML Nat.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 \
- Tools/Presburger/reflected_presburger.ML Tools/cnf_funcs.ML \
- Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
- Tools/datatype_case.ML Tools/datatype_codegen.ML \
+ ATP_Linkup.thy Accessible_Part.thy Code_Generator.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 \
+ 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 \
@@ -130,7 +127,7 @@
Tools/typedef_codegen.ML Tools/typedef_package.ML \
Transitive_Closure.thy Typedef.thy Wellfounded_Recursion.thy \
Wellfounded_Relations.thy arith_data.ML document/root.tex hologic.ML \
- simpdata.ML
+ int_arith1.ML int_factor_simprocs.ML nat_simprocs.ML simpdata.ML
@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL
@@ -422,7 +419,7 @@
Auth/Guard/Proto.thy Auth/Guard/Guard_Yahalom.thy\
Auth/Smartcard/EventSC.thy Auth/Smartcard/ShoupRubinBella.thy\
Auth/Smartcard/ShoupRubin.thy Auth/Smartcard/Smartcard.thy\
- Auth/document/root.tex
+ Auth/document/root.tex
@$(ISATOOL) usedir -g true $(OUT)/HOL Auth