| changeset 63834 | 6a757f36997e |
| parent 63714 | b62f4f765353 |
| child 66198 | 4a5589dd8e1a |
--- a/src/HOL/BNF_Def.thy Sun Sep 11 00:14:37 2016 +0200 +++ b/src/HOL/BNF_Def.thy Sun Sep 11 00:14:44 2016 +0200 @@ -200,7 +200,7 @@ by (simp add: the_inv_f_f) lemma vimage2pI: "R (f x) (g y) \<Longrightarrow> vimage2p f g R x y" - unfolding vimage2p_def by - + unfolding vimage2p_def . lemma rel_fun_iff_leq_vimage2p: "(rel_fun R S) f g = (R \<le> vimage2p f g S)" unfolding rel_fun_def vimage2p_def by auto