src/HOL/Transfer.thy
changeset 57398 882091eb1e9a
parent 57260 8747af0d1012
child 57599 7ef939f89776
     1.1 --- a/src/HOL/Transfer.thy	Fri Jun 27 10:11:44 2014 +0200
     1.2 +++ b/src/HOL/Transfer.thy	Fri Jun 27 10:11:44 2014 +0200
     1.3 @@ -230,7 +230,7 @@
     1.4  definition eq_onp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 
     1.5    where "eq_onp R = (\<lambda>x y. R x \<and> x = y)"
     1.6  
     1.7 -lemma eq_onp_Grp: "eq_onp P = BNF_Util.Grp (Collect P) id" 
     1.8 +lemma eq_onp_Grp: "eq_onp P = BNF_Def.Grp (Collect P) id" 
     1.9  unfolding eq_onp_def Grp_def by auto 
    1.10  
    1.11  lemma eq_onp_to_eq: