# HG changeset patch # User blanchet # Date 1347376489 -7200 # Node ID 97809ae5f7bb1cc9eb239e063da453ba6b8a7275 # Parent c057e1b39f162cfdecf7c97f48c12661f7d529fe move "bnf_util.ML" to "BNF_Util.thy" diff -r c057e1b39f16 -r 97809ae5f7bb src/HOL/Codatatype/BNF_Def.thy --- a/src/HOL/Codatatype/BNF_Def.thy Tue Sep 11 17:09:39 2012 +0200 +++ b/src/HOL/Codatatype/BNF_Def.thy Tue Sep 11 17:14:49 2012 +0200 @@ -14,8 +14,6 @@ and "bnf_def" :: thy_goal uses - "Tools/bnf_util.ML" - "Tools/bnf_tactics.ML" "Tools/bnf_def.ML" begin diff -r c057e1b39f16 -r 97809ae5f7bb src/HOL/Codatatype/BNF_Util.thy --- a/src/HOL/Codatatype/BNF_Util.thy Tue Sep 11 17:09:39 2012 +0200 +++ b/src/HOL/Codatatype/BNF_Util.thy Tue Sep 11 17:14:49 2012 +0200 @@ -13,6 +13,8 @@ "../Ordinals_and_Cardinals/Cardinal_Arithmetic" "~~/src/HOL/Library/Prefix_Order" Equiv_Relations_More +uses + ("Tools/bnf_util.ML") begin lemma iffI_np: "\x \ \ y; \ x \ y\ \ \ x \ y" @@ -851,4 +853,7 @@ lemma not_arg_cong_Inr: "x \ y \ Inr x \ Inr y" by simp +ML_file "Tools/bnf_util.ML" +ML_file "Tools/bnf_tactics.ML" + end diff -r c057e1b39f16 -r 97809ae5f7bb src/HOL/Codatatype/BNF_Wrap.thy --- a/src/HOL/Codatatype/BNF_Wrap.thy Tue Sep 11 17:09:39 2012 +0200 +++ b/src/HOL/Codatatype/BNF_Wrap.thy Tue Sep 11 17:14:49 2012 +0200 @@ -8,7 +8,7 @@ header {* Wrapping Datatypes *} theory BNF_Wrap -imports BNF_Def +imports BNF_Util keywords "wrap_data" :: thy_goal and diff -r c057e1b39f16 -r 97809ae5f7bb src/HOL/Codatatype/Codatatype.thy --- a/src/HOL/Codatatype/Codatatype.thy Tue Sep 11 17:09:39 2012 +0200 +++ b/src/HOL/Codatatype/Codatatype.thy Tue Sep 11 17:14:49 2012 +0200 @@ -10,7 +10,7 @@ header {* The (Co)datatype Package *} theory Codatatype -imports BNF_Wrap BNF_LFP BNF_GFP +imports BNF_LFP BNF_GFP BNF_Wrap keywords "data" :: thy_decl and