--- 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
--- 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
--- 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
--- 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