src/HOL/Quotient_Examples/Cset.thy
changeset 44928 7ef6505bde7f
parent 44860 56101fa00193
--- a/src/HOL/Quotient_Examples/Cset.thy	Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/Quotient_Examples/Cset.thy	Wed Sep 14 10:08:52 2011 -0400
@@ -97,6 +97,6 @@
 hide_fact (open) is_empty_def insert_def remove_def map_def filter_def
   forall_def exists_def card_def set_def subset_def psubset_def
   inter_def union_def empty_def UNIV_def uminus_def minus_def Inf_def Sup_def
-  UNION_def
+  UNION_eq
 
 end