src/HOL/BNF/BNF_Util.thy
changeset 51893 596baae88a88
parent 49510 ba50d204095e
child 53560 4b5f42cfa244
     1.1 --- a/src/HOL/BNF/BNF_Util.thy	Tue May 07 11:27:29 2013 +0200
     1.2 +++ b/src/HOL/BNF/BNF_Util.thy	Tue May 07 14:22:54 2013 +0200
     1.3 @@ -60,6 +60,8 @@
     1.4  (* Operator: *)
     1.5  definition "Gr A f = {(a, f a) | a. a \<in> A}"
     1.6  
     1.7 +definition "Grp A f = (\<lambda>a b. b = f a \<and> a \<in> A)"
     1.8 +
     1.9  ML_file "Tools/bnf_util.ML"
    1.10  ML_file "Tools/bnf_tactics.ML"
    1.11