--- a/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy Tue Aug 19 09:34:27 2014 +0200
+++ b/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy Tue Aug 19 09:34:30 2014 +0200
@@ -47,13 +47,13 @@
using Node unfolding Node_def
by (metis Node Node_root_cont finite_cont)
-lemma dtree_sel_ctor[simp]:
+lemma dtree_sel_ctr[simp]:
"root (Node n as) = n"
"finite as \<Longrightarrow> cont (Node n as) = as"
unfolding Node_def cont_def by auto
-lemmas root_Node = dtree_sel_ctor(1)
-lemmas cont_Node = dtree_sel_ctor(2)
+lemmas root_Node = dtree_sel_ctr(1)
+lemmas cont_Node = dtree_sel_ctr(2)
lemma dtree_cong:
assumes "root tr = root tr'" and "cont tr = cont tr'"
--- a/src/HOL/BNF_GFP.thy Tue Aug 19 09:34:27 2014 +0200
+++ b/src/HOL/BNF_GFP.thy Tue Aug 19 09:34:30 2014 +0200
@@ -285,12 +285,12 @@
qed
lemma univ_preserves:
- assumes ECH: "equiv A r" and RES: "f respects r" and PRES: "\<forall> x \<in> A. f x \<in> B"
+ assumes ECH: "equiv A r" and RES: "f respects r" and PRES: "\<forall>x \<in> A. f x \<in> B"
shows "\<forall>X \<in> A//r. univ f X \<in> B"
proof
fix X assume "X \<in> A//r"
then obtain x where x: "x \<in> A" and X: "X = proj r x" using ECH proj_image[of r A] by blast
- hence "univ f X = f x" using assms univ_commute by fastforce
+ hence "univ f X = f x" using ECH RES univ_commute by fastforce
thus "univ f X \<in> B" using x PRES by simp
qed
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Tue Aug 19 09:34:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Tue Aug 19 09:34:30 2014 +0200
@@ -2514,12 +2514,7 @@
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
bs thmss);
- (*FIXME: once the package exports all the necessary high-level characteristic theorems,
- those should not only be concealed but rather not noted at all*)
- val maybe_conceal_notes = note_all = false ? map (apfst (apfst Binding.conceal));
-
- val (noted, lthy') =
- lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Jbnf_notes));
+ val lthy' = lthy |> note_all ? snd o Local_Theory.notes (common_notes @ notes @ Jbnf_notes);
val fp_res =
{Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_co_recs = corecs,
@@ -2528,8 +2523,7 @@
xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss',
xtor_rel_thms = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms,
xtor_co_rec_o_map_thms = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm,
- dtor_set_induct_thms = dtor_Jset_induct_thms}
- |> morph_fp_result (substitute_noted_thm noted);
+ dtor_set_induct_thms = dtor_Jset_induct_thms};
in
timer; (fp_res, lthy')
end;
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Tue Aug 19 09:34:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Tue Aug 19 09:34:30 2014 +0200
@@ -1801,12 +1801,7 @@
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
bs thmss);
- (*FIXME: once the package exports all the necessary high-level characteristic theorems,
- those should not only be concealed but rather not noted at all*)
- val maybe_conceal_notes = note_all = false ? map (apfst (apfst Binding.conceal));
-
- val (noted, lthy') =
- lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Ibnf_notes));
+ val lthy' = lthy |> note_all ? snd o Local_Theory.notes (common_notes @ notes @ Ibnf_notes);
val fp_res =
{Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_recs = recs,
@@ -1815,8 +1810,7 @@
xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss',
xtor_rel_thms = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms,
xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm,
- dtor_set_induct_thms = []}
- |> morph_fp_result (substitute_noted_thm noted);
+ dtor_set_induct_thms = []};
in
timer; (fp_res, lthy')
end;