src/HOL/BNF_LFP.thy
changeset 55084 8ee9aabb2bca
parent 55066 4e5ddf3162ac
child 55530 3dfb724db099
--- a/src/HOL/BNF_LFP.thy	Mon Jan 20 20:21:12 2014 +0100
+++ b/src/HOL/BNF_LFP.thy	Mon Jan 20 20:42:43 2014 +0100
@@ -222,7 +222,7 @@
 lemma meta_spec2:
   assumes "(\<And>x y. PROP P x y)"
   shows "PROP P x y"
-by (rule `(\<And>x y. PROP P x y)`)
+by (rule assms)
 
 lemma nchotomy_relcomppE:
   "\<lbrakk>\<And>y. \<exists>x. y = f x; (r OO s) a c; \<And>b. r a (f b) \<Longrightarrow> s (f b) c \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
@@ -234,10 +234,15 @@
 lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> S (f x) (g y)"
   unfolding vimage2p_def by auto
 
+lemma id_transfer: "fun_rel A A id id"
+unfolding fun_rel_def by simp
+
 ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML"
 ML_file "Tools/BNF/bnf_lfp_util.ML"
 ML_file "Tools/BNF/bnf_lfp_tactics.ML"
 ML_file "Tools/BNF/bnf_lfp.ML"
 ML_file "Tools/BNF/bnf_lfp_compat.ML"
 
+hide_fact (open) id_transfer
+
 end