# HG changeset patch # User Christian Urban # Date 1349351083 -3600 # Node ID 3e6f4320669f474e270583f41b03636eee35a16a # Parent 995d47b09ab422aefba6b52b1da2536f0143dfc2 removed "use" - replaced by "ML_file" diff -r 995d47b09ab4 -r 3e6f4320669f Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Thu Oct 04 11:10:23 2012 +0100 +++ b/Nominal/Nominal2.thy Thu Oct 04 12:44:43 2012 +0100 @@ -5,51 +5,40 @@ "nominal_datatype" :: thy_decl and "nominal_primrec" "nominal_inductive" :: thy_goal and "avoids" "binds" -uses ("nominal_dt_rawfuns.ML") - ("nominal_dt_alpha.ML") - ("nominal_dt_quot.ML") - ("nominal_induct.ML") - ("nominal_inductive.ML") - ("nominal_function_common.ML") - ("nominal_function_core.ML") - ("nominal_mutual.ML") - ("nominal_function.ML") - ("nominal_termination.ML") - ("nominal_dt_data.ML") begin -use "nominal_dt_data.ML" +ML_file "nominal_dt_data.ML" ML {* open Nominal_Dt_Data *} -use "nominal_dt_rawfuns.ML" +ML_file "nominal_dt_rawfuns.ML" ML {* open Nominal_Dt_RawFuns *} -use "nominal_dt_alpha.ML" +ML_file "nominal_dt_alpha.ML" ML {* open Nominal_Dt_Alpha *} -use "nominal_dt_quot.ML" +ML_file "nominal_dt_quot.ML" ML {* open Nominal_Dt_Quot *} (*****************************************) (* setup for induction principles method *) -use "nominal_induct.ML" +ML_file "nominal_induct.ML" method_setup nominal_induct = {* NominalInduct.nominal_induct_method *} {* nominal induction *} (****************************************************) (* inductive definition involving nominal datatypes *) -use "nominal_inductive.ML" +ML_file "nominal_inductive.ML" (***************************************) (* forked code of the function package *) (* for defining nominal functions *) -use "nominal_function_common.ML" -use "nominal_function_core.ML" -use "nominal_mutual.ML" -use "nominal_function.ML" -use "nominal_termination.ML" +ML_file "nominal_function_common.ML" +ML_file "nominal_function_core.ML" +ML_file "nominal_mutual.ML" +ML_file "nominal_function.ML" +ML_file "nominal_termination.ML" ML {* val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) diff -r 995d47b09ab4 -r 3e6f4320669f Nominal/Nominal2_Base.thy --- a/Nominal/Nominal2_Base.thy Thu Oct 04 11:10:23 2012 +0100 +++ b/Nominal/Nominal2_Base.thy Thu Oct 04 12:44:43 2012 +0100 @@ -11,12 +11,6 @@ "~~/src/HOL/Library/FinFun" keywords "atom_decl" "equivariance" :: thy_decl -uses ("nominal_basics.ML") - ("nominal_thmdecls.ML") - ("nominal_permeq.ML") - ("nominal_library.ML") - ("nominal_atoms.ML") - ("nominal_eqvt.ML") begin section {* Atoms and Sorts *} @@ -768,14 +762,14 @@ subsection {* Basic functions about permutations *} -use "nominal_basics.ML" +ML_file "nominal_basics.ML" subsection {* Eqvt infrastructure *} text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *} -use "nominal_thmdecls.ML" +ML_file "nominal_thmdecls.ML" setup "Nominal_ThmDecls.setup" @@ -817,7 +811,7 @@ text {* provides perm_simp methods *} -use "nominal_permeq.ML" +ML_file "nominal_permeq.ML" method_setup perm_simp = {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *} @@ -3235,7 +3229,7 @@ section {* Library functions for the nominal infrastructure *} -use "nominal_library.ML" +ML_file "nominal_library.ML" @@ -3425,12 +3419,12 @@ text {* at the moment only single-sort concrete atoms are supported *} -use "nominal_atoms.ML" +ML_file "nominal_atoms.ML" section {* automatic equivariance procedure for inductive definitions *} -use "nominal_eqvt.ML" +ML_file "nominal_eqvt.ML"