src/HOL/Inductive.thy
changeset 48891 c0eafbd55de3
parent 48357 828ace4f75ab
child 50302 9149a07a6c67
     1.1 --- a/src/HOL/Inductive.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -11,15 +11,6 @@
     1.4    "inductive_cases" "inductive_simps" :: thy_script and "monos" and
     1.5    "rep_datatype" :: thy_goal and
     1.6    "primrec" :: thy_decl
     1.7 -uses
     1.8 -  ("Tools/inductive.ML")
     1.9 -  ("Tools/Datatype/datatype_aux.ML")
    1.10 -  ("Tools/Datatype/datatype_prop.ML")
    1.11 -  ("Tools/Datatype/datatype_data.ML")
    1.12 -  ("Tools/Datatype/datatype_case.ML")
    1.13 -  ("Tools/Datatype/rep_datatype.ML")
    1.14 -  ("Tools/Datatype/datatype_codegen.ML")
    1.15 -  ("Tools/Datatype/primrec.ML")
    1.16  begin
    1.17  
    1.18  subsection {* Least and greatest fixed points *}
    1.19 @@ -264,7 +255,7 @@
    1.20    subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
    1.21    Collect_mono in_mono vimage_mono
    1.22  
    1.23 -use "Tools/inductive.ML"
    1.24 +ML_file "Tools/inductive.ML"
    1.25  setup Inductive.setup
    1.26  
    1.27  theorems [mono] =
    1.28 @@ -278,13 +269,13 @@
    1.29  
    1.30  text {* Package setup. *}
    1.31  
    1.32 -use "Tools/Datatype/datatype_aux.ML"
    1.33 -use "Tools/Datatype/datatype_prop.ML"
    1.34 -use "Tools/Datatype/datatype_data.ML" setup Datatype_Data.setup
    1.35 -use "Tools/Datatype/datatype_case.ML" setup Datatype_Case.setup
    1.36 -use "Tools/Datatype/rep_datatype.ML"
    1.37 -use "Tools/Datatype/datatype_codegen.ML" setup Datatype_Codegen.setup
    1.38 -use "Tools/Datatype/primrec.ML"
    1.39 +ML_file "Tools/Datatype/datatype_aux.ML"
    1.40 +ML_file "Tools/Datatype/datatype_prop.ML"
    1.41 +ML_file "Tools/Datatype/datatype_data.ML" setup Datatype_Data.setup
    1.42 +ML_file "Tools/Datatype/datatype_case.ML" setup Datatype_Case.setup
    1.43 +ML_file "Tools/Datatype/rep_datatype.ML"
    1.44 +ML_file "Tools/Datatype/datatype_codegen.ML" setup Datatype_Codegen.setup
    1.45 +ML_file "Tools/Datatype/primrec.ML"
    1.46  
    1.47  text{* Lambda-abstractions with pattern matching: *}
    1.48