src/HOL/BNF_Util.thy
changeset 55803 74d3fe9031d8
parent 55084 8ee9aabb2bca
child 55945 e96383acecf9
--- a/src/HOL/BNF_Util.thy	Fri Feb 28 12:04:40 2014 +0100
+++ b/src/HOL/BNF_Util.thy	Tue Feb 25 18:14:26 2014 +0100
@@ -44,6 +44,9 @@
 
 definition "Grp A f = (\<lambda>a b. b = f a \<and> a \<in> A)"
 
+definition vimage2p where
+  "vimage2p f g R = (\<lambda>x y. R (f x) (g y))"
+
 ML_file "Tools/BNF/bnf_util.ML"
 ML_file "Tools/BNF/bnf_tactics.ML"