| changeset 57398 | 882091eb1e9a |
| parent 55934 | 800e155d051a |
| child 58881 | b9556a055632 |
--- a/src/HOL/Library/Countable_Set_Type.thy Fri Jun 27 10:11:44 2014 +0200 +++ b/src/HOL/Library/Countable_Set_Type.thy Fri Jun 27 10:11:44 2014 +0200 @@ -11,7 +11,7 @@ imports Countable_Set Cardinal_Notations begin -abbreviation "Grp \<equiv> BNF_Util.Grp" +abbreviation "Grp \<equiv> BNF_Def.Grp" subsection{* Cardinal stuff *}