--- a/src/HOL/BNF/BNF_FP_Basic.thy Fri Aug 30 12:06:37 2013 +0200
+++ b/src/HOL/BNF/BNF_FP_Basic.thy Fri Aug 30 12:09:51 2013 +0200
@@ -156,6 +156,13 @@
lemma eq_subset: "op = \<le> (\<lambda>a b. P a b \<or> a = b)"
by auto
+lemma eq_le_Grp_id_iff: "(op = \<le> Grp (Collect R) id) = (All R)"
+ unfolding Grp_def id_apply by blast
+
+lemma Grp_id_mono_subst: "(\<And>x y. Grp P id x y \<Longrightarrow> Grp Q id (f x) (f y)) \<equiv>
+ (\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)"
+ unfolding Grp_def by rule 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')"
@@ -169,6 +176,9 @@
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_n2m_tactics.ML"
+ML_file "Tools/bnf_fp_n2m.ML"
+ML_file "Tools/bnf_fp_n2m_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"
--- a/src/HOL/BNF/BNF_FP_N2M.thy Fri Aug 30 12:06:37 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-(* Title: HOL/BNF/BNF_FP_N2M.thy
- Author: Dmitriy Traytel, TU Muenchen
- Author: Jasmin Blanchette, TU Muenchen
- Copyright 2013
-
-Flattening of nested to mutual (co)recursion.
-*)
-
-header {* Flattening of Nested to Mutual (Co)recursion *}
-
-theory BNF_FP_N2M
-imports BNF_FP_Basic
-begin
-
-lemma eq_le_Grp_id_iff: "(op = \<le> BNF_Util.Grp (Collect R) id) = (All R)"
- unfolding Grp_def id_apply by blast
-
-lemma Grp_id_mono_subst: "(\<And>x y. BNF_Util.Grp P id x y \<Longrightarrow> BNF_Util.Grp Q id (f x) (f y)) \<equiv>
- (\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)"
- unfolding Grp_def by rule auto
-
-ML_file "Tools/bnf_fp_n2m_tactics.ML"
-ML_file "Tools/bnf_fp_n2m.ML"
-ML_file "Tools/bnf_fp_n2m_sugar.ML"
-
-end