src/HOL/BNF_LFP.thy
changeset 55084 8ee9aabb2bca
parent 55066 4e5ddf3162ac
child 55530 3dfb724db099
     1.1 --- a/src/HOL/BNF_LFP.thy	Mon Jan 20 20:21:12 2014 +0100
     1.2 +++ b/src/HOL/BNF_LFP.thy	Mon Jan 20 20:42:43 2014 +0100
     1.3 @@ -222,7 +222,7 @@
     1.4  lemma meta_spec2:
     1.5    assumes "(\<And>x y. PROP P x y)"
     1.6    shows "PROP P x y"
     1.7 -by (rule `(\<And>x y. PROP P x y)`)
     1.8 +by (rule assms)
     1.9  
    1.10  lemma nchotomy_relcomppE:
    1.11    "\<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"
    1.12 @@ -234,10 +234,15 @@
    1.13  lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> S (f x) (g y)"
    1.14    unfolding vimage2p_def by auto
    1.15  
    1.16 +lemma id_transfer: "fun_rel A A id id"
    1.17 +unfolding fun_rel_def by simp
    1.18 +
    1.19  ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML"
    1.20  ML_file "Tools/BNF/bnf_lfp_util.ML"
    1.21  ML_file "Tools/BNF/bnf_lfp_tactics.ML"
    1.22  ML_file "Tools/BNF/bnf_lfp.ML"
    1.23  ML_file "Tools/BNF/bnf_lfp_compat.ML"
    1.24  
    1.25 +hide_fact (open) id_transfer
    1.26 +
    1.27  end