# HG changeset patch
# User blanchet
# Date 1377857122 -7200
# Node ID 29c267cb9314a948302774b1ff7f94684b826f6d
# Parent  cfef783090ebf5d32fd84f51f34e19a0bce86de6
rationalized files

diff -r cfef783090eb -r 29c267cb9314 src/HOL/BNF/BNF_FP_Basic.thy
--- a/src/HOL/BNF/BNF_FP_Basic.thy	Fri Aug 30 11:37:22 2013 +0200
+++ b/src/HOL/BNF/BNF_FP_Basic.thy	Fri Aug 30 12:05:22 2013 +0200
@@ -11,7 +11,10 @@
 theory BNF_FP_Basic
 imports BNF_Comp BNF_Ctr_Sugar
 keywords
-  "defaults"
+  "primrec_new" :: thy_decl and
+  "primcorec" :: thy_goal and
+  "defaults" and
+  "sequential"
 begin
 
 lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
@@ -153,8 +156,21 @@
 lemma eq_subset: "op = \<le> (\<lambda>a b. P a b \<or> a = b)"
   by auto
 
+lemma if_if_True:
+  "(if (if b then True else b') then (if b then x else x') else f (if b then y else y')) =
+   (if b then x else if b' then x' else f y')"
+  by simp
+
+lemma if_if_False:
+  "(if (if b then False else b') then (if b then x else x') else f (if b then y else y')) =
+   (if b then f y else if b' then x' else f y')"
+  by simp
+
 ML_file "Tools/bnf_fp_util.ML"
 ML_file "Tools/bnf_fp_def_sugar_tactics.ML"
 ML_file "Tools/bnf_fp_def_sugar.ML"
+ML_file "Tools/bnf_fp_rec_sugar_util.ML"
+ML_file "Tools/bnf_fp_rec_sugar_tactics.ML"
+ML_file "Tools/bnf_fp_rec_sugar.ML"
 
 end
diff -r cfef783090eb -r 29c267cb9314 src/HOL/BNF/BNF_FP_Rec_Sugar.thy
--- a/src/HOL/BNF/BNF_FP_Rec_Sugar.thy	Fri Aug 30 11:37:22 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-(*  Title:      HOL/BNF/BNF_FP_Rec_Sugar.thy
-    Author:     Lorenz Panny, TU Muenchen
-    Author:     Jasmin Blanchette, TU Muenchen
-    Author:     Dmitriy Traytel, TU Muenchen
-    Copyright   2013
-
-Recursor and corecursor sugar.
-*)
-
-header {* Recursor and Corecursor Sugar *}
-
-theory BNF_FP_Rec_Sugar
-imports BNF_FP_N2M
-keywords
-  "primrec_new" :: thy_decl and
-  "primcorec" :: thy_goal and
-  "sequential"
-begin
-
-lemma if_if_True:
-"(if (if b then True else b') then (if b then x else x') else f (if b then y else y')) =
- (if b then x else if b' then x' else f y')"
-by simp
-
-lemma if_if_False:
-"(if (if b then False else b') then (if b then x else x') else f (if b then y else y')) =
- (if b then f y else if b' then x' else f y')"
-by simp
-
-ML_file "Tools/bnf_fp_rec_sugar_util.ML"
-ML_file "Tools/bnf_fp_rec_sugar_tactics.ML"
-ML_file "Tools/bnf_fp_rec_sugar.ML"
-
-end
diff -r cfef783090eb -r 29c267cb9314 src/HOL/BNF/BNF_LFP.thy
--- a/src/HOL/BNF/BNF_LFP.thy	Fri Aug 30 11:37:22 2013 +0200
+++ b/src/HOL/BNF/BNF_LFP.thy	Fri Aug 30 12:05:22 2013 +0200
@@ -1,6 +1,8 @@
 (*  Title:      HOL/BNF/BNF_LFP.thy
     Author:     Dmitriy Traytel, TU Muenchen
-    Copyright   2012
+    Author:     Lorenz Panny, TU Muenchen
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2012, 2013
 
 Least fixed point operation on bounded natural functors.
 *)
@@ -10,7 +12,8 @@
 theory BNF_LFP
 imports BNF_FP_Basic
 keywords
-  "datatype_new" :: thy_decl
+  "datatype_new" :: thy_decl and
+  "datatype_compat" :: thy_decl
 begin
 
 lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
@@ -232,5 +235,6 @@
 ML_file "Tools/bnf_lfp_util.ML"
 ML_file "Tools/bnf_lfp_tactics.ML"
 ML_file "Tools/bnf_lfp.ML"
+ML_file "Tools/bnf_lfp_compat.ML"
 
 end
diff -r cfef783090eb -r 29c267cb9314 src/HOL/BNF/BNF_LFP_Compat.thy
--- a/src/HOL/BNF/BNF_LFP_Compat.thy	Fri Aug 30 11:37:22 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-(*  Title:      HOL/BNF/BNF_LFP_Compat.thy
-    Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2013
-
-Compatibility layer with the old datatype package.
-*)
-
-header {* Compatibility Layer with the Old Datatype Package *}
-
-theory BNF_LFP_Compat
-imports BNF_FP_N2M
-keywords
-  "datatype_compat" :: thy_goal
-begin
-
-ML_file "Tools/bnf_lfp_compat.ML"
-
-end