| changeset 54485 | b61b8c9e4cf7 |
| parent 54421 | 632be352a5a3 |
| child 54581 | 1502a1f707d9 |
--- a/src/HOL/BNF/BNF_Def.thy Tue Nov 19 01:29:50 2013 +0100 +++ b/src/HOL/BNF/BNF_Def.thy Tue Nov 19 01:30:14 2013 +0100 @@ -190,9 +190,6 @@ lemma vimage2pI: "R (f x) (g y) \<Longrightarrow> vimage2p f g R x y" unfolding vimage2p_def by - -lemma vimage2pD: "vimage2p f g R x y \<Longrightarrow> R (f x) (g y)" - unfolding vimage2p_def by - - lemma fun_rel_iff_leq_vimage2p: "(fun_rel R S) f g = (R \<le> vimage2p f g S)" unfolding fun_rel_def vimage2p_def by auto