src/HOL/BNF_LFP.thy
changeset 55066 4e5ddf3162ac
parent 55062 6d3fad6f01c9
child 55084 8ee9aabb2bca
     1.1 --- a/src/HOL/BNF_LFP.thy	Mon Jan 20 18:24:56 2014 +0100
     1.2 +++ b/src/HOL/BNF_LFP.thy	Mon Jan 20 18:24:56 2014 +0100
     1.3 @@ -225,10 +225,10 @@
     1.4  by (rule `(\<And>x y. PROP P x y)`)
     1.5  
     1.6  lemma nchotomy_relcomppE:
     1.7 -  "\<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.8 +  "\<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.9    by (metis relcompp.cases)
    1.10  
    1.11 -lemma vimage2p_fun_rel: "(fun_rel (vimage2p f g R) R) f g"
    1.12 +lemma vimage2p_fun_rel: "fun_rel (vimage2p f g R) R f g"
    1.13    unfolding fun_rel_def vimage2p_def by auto
    1.14  
    1.15  lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> S (f x) (g y)"