move "bnf_util.ML" to "BNF_Util.thy"
authorblanchet
Tue Sep 11 17:14:49 2012 +0200 (2012-09-11)
changeset 4928397809ae5f7bb
parent 49282 c057e1b39f16
child 49284 5f39b7940b49
move "bnf_util.ML" to "BNF_Util.thy"
src/HOL/Codatatype/BNF_Def.thy
src/HOL/Codatatype/BNF_Util.thy
src/HOL/Codatatype/BNF_Wrap.thy
src/HOL/Codatatype/Codatatype.thy
     1.1 --- a/src/HOL/Codatatype/BNF_Def.thy	Tue Sep 11 17:09:39 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/BNF_Def.thy	Tue Sep 11 17:14:49 2012 +0200
     1.3 @@ -14,8 +14,6 @@
     1.4  and
     1.5    "bnf_def" :: thy_goal
     1.6  uses
     1.7 -  "Tools/bnf_util.ML"
     1.8 -  "Tools/bnf_tactics.ML"
     1.9    "Tools/bnf_def.ML"
    1.10  begin
    1.11  
     2.1 --- a/src/HOL/Codatatype/BNF_Util.thy	Tue Sep 11 17:09:39 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/BNF_Util.thy	Tue Sep 11 17:14:49 2012 +0200
     2.3 @@ -13,6 +13,8 @@
     2.4    "../Ordinals_and_Cardinals/Cardinal_Arithmetic"
     2.5    "~~/src/HOL/Library/Prefix_Order"
     2.6    Equiv_Relations_More
     2.7 +uses
     2.8 +  ("Tools/bnf_util.ML")
     2.9  begin
    2.10  
    2.11  lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
    2.12 @@ -851,4 +853,7 @@
    2.13  lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
    2.14  by simp
    2.15  
    2.16 +ML_file "Tools/bnf_util.ML"
    2.17 +ML_file "Tools/bnf_tactics.ML"
    2.18 +
    2.19  end
     3.1 --- a/src/HOL/Codatatype/BNF_Wrap.thy	Tue Sep 11 17:09:39 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/BNF_Wrap.thy	Tue Sep 11 17:14:49 2012 +0200
     3.3 @@ -8,7 +8,7 @@
     3.4  header {* Wrapping Datatypes *}
     3.5  
     3.6  theory BNF_Wrap
     3.7 -imports BNF_Def
     3.8 +imports BNF_Util
     3.9  keywords
    3.10    "wrap_data" :: thy_goal
    3.11  and
     4.1 --- a/src/HOL/Codatatype/Codatatype.thy	Tue Sep 11 17:09:39 2012 +0200
     4.2 +++ b/src/HOL/Codatatype/Codatatype.thy	Tue Sep 11 17:14:49 2012 +0200
     4.3 @@ -10,7 +10,7 @@
     4.4  header {* The (Co)datatype Package *}
     4.5  
     4.6  theory Codatatype
     4.7 -imports BNF_Wrap BNF_LFP BNF_GFP
     4.8 +imports BNF_LFP BNF_GFP BNF_Wrap
     4.9  keywords
    4.10    "data" :: thy_decl
    4.11  and