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