src/HOL/IsaMakefile
changeset 31723 f5cafe803b55
parent 31706 1db0c8f235fb
child 31726 ffd2dc631d88
     1.1 --- a/src/HOL/IsaMakefile	Thu Jun 18 18:31:14 2009 -0700
     1.2 +++ b/src/HOL/IsaMakefile	Fri Jun 19 17:23:21 2009 +0200
     1.3 @@ -145,7 +145,7 @@
     1.4    Tools/datatype_package/datatype_aux.ML \
     1.5    Tools/datatype_package/datatype_case.ML \
     1.6    Tools/datatype_package/datatype_codegen.ML \
     1.7 -  Tools/datatype_package/datatype_package.ML \
     1.8 +  Tools/datatype_package/datatype.ML \
     1.9    Tools/datatype_package/datatype_prop.ML \
    1.10    Tools/datatype_package/datatype_realizer.ML \
    1.11    Tools/datatype_package/datatype_rep_proofs.ML \
    1.12 @@ -158,7 +158,7 @@
    1.13    Tools/function_package/fundef_core.ML \
    1.14    Tools/function_package/fundef_datatype.ML \
    1.15    Tools/function_package/fundef_lib.ML \
    1.16 -  Tools/function_package/fundef_package.ML \
    1.17 +  Tools/function_package/fundef.ML \
    1.18    Tools/function_package/induction_scheme.ML \
    1.19    Tools/function_package/inductive_wrap.ML \
    1.20    Tools/function_package/lexicographic_order.ML \
    1.21 @@ -171,24 +171,24 @@
    1.22    Tools/function_package/sum_tree.ML \
    1.23    Tools/function_package/termination.ML \
    1.24    Tools/inductive_codegen.ML \
    1.25 -  Tools/inductive_package.ML \
    1.26 +  Tools/inductive.ML \
    1.27    Tools/inductive_realizer.ML \
    1.28 -  Tools/inductive_set_package.ML \
    1.29 +  Tools/inductive_set.ML \
    1.30    Tools/lin_arith.ML \
    1.31    Tools/nat_arith.ML \
    1.32 -  Tools/old_primrec_package.ML \
    1.33 -  Tools/primrec_package.ML \
    1.34 +  Tools/old_primrec.ML \
    1.35 +  Tools/primrec.ML \
    1.36    Tools/prop_logic.ML \
    1.37 -  Tools/record_package.ML \
    1.38 +  Tools/record.ML \
    1.39    Tools/refute.ML \
    1.40    Tools/refute_isar.ML \
    1.41    Tools/rewrite_hol_proof.ML \
    1.42    Tools/sat_funcs.ML \
    1.43    Tools/sat_solver.ML \
    1.44    Tools/split_rule.ML \
    1.45 -  Tools/typecopy_package.ML \
    1.46 +  Tools/typecopy.ML \
    1.47    Tools/typedef_codegen.ML \
    1.48 -  Tools/typedef_package.ML \
    1.49 +  Tools/typedef.ML \
    1.50    Transitive_Closure.thy \
    1.51    Typedef.thy \
    1.52    Wellfounded.thy \
    1.53 @@ -250,13 +250,13 @@
    1.54    Tools/Qelim/generated_cooper.ML \
    1.55    Tools/Qelim/presburger.ML \
    1.56    Tools/Qelim/qelim.ML \
    1.57 -  Tools/recdef_package.ML \
    1.58 +  Tools/recdef.ML \
    1.59    Tools/res_atp.ML \
    1.60    Tools/res_axioms.ML \
    1.61    Tools/res_clause.ML \
    1.62    Tools/res_hol_clause.ML \
    1.63    Tools/res_reconstruct.ML \
    1.64 -  Tools/specification_package.ML \
    1.65 +  Tools/choice_specification.ML \
    1.66    Tools/string_code.ML \
    1.67    Tools/string_syntax.ML \
    1.68    Tools/TFL/casesplit.ML \
    1.69 @@ -423,7 +423,7 @@
    1.70  IMPORTER_FILES = Import/lazy_seq.ML Import/proof_kernel.ML Import/replay.ML \
    1.71    Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \
    1.72    Import/HOL4Syntax.thy Import/HOL4Compat.thy Import/import_syntax.ML \
    1.73 -  Import/hol4rews.ML Import/import_package.ML Import/ROOT.ML
    1.74 +  Import/hol4rews.ML Import/import.ML Import/ROOT.ML
    1.75  
    1.76  IMPORTER_HOLLIGHT_FILES = Import/proof_kernel.ML Import/replay.ML \
    1.77    Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \
    1.78 @@ -968,7 +968,7 @@
    1.79    Nominal/nominal_induct.ML \
    1.80    Nominal/nominal_inductive.ML \
    1.81    Nominal/nominal_inductive2.ML \
    1.82 -  Nominal/nominal_package.ML \
    1.83 +  Nominal/nominal.ML \
    1.84    Nominal/nominal_permeq.ML \
    1.85    Nominal/nominal_primrec.ML \
    1.86    Nominal/nominal_thmdecls.ML \