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"