# HG changeset patch
# User blanchet
# Date 1377857391 -7200
# Node ID d066e4923a315168daba722d7af39414c72a7408
# Parent  221ff2b39a3533c9149589d468fd0a5dd783e466
merged two theory files

diff -r 221ff2b39a35 -r d066e4923a31 src/HOL/BNF/BNF_FP_Basic.thy
--- 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"
diff -r 221ff2b39a35 -r d066e4923a31 src/HOL/BNF/BNF_FP_N2M.thy
--- 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