1.1 --- a/src/HOL/Fun.ML	Tue Apr 23 16:44:22 1996 +0200
     1.2 +++ b/src/HOL/Fun.ML	Tue Apr 23 16:58:21 1996 +0200
     1.3 @@ -186,10 +186,10 @@
     1.4  fun prover s = prove_goal Fun.thy s (fn _=>[fast_tac set_cs 1]);
     1.5  
     1.6  val mem_simps = map prover
     1.7 - [ "(a : A Un B)   =  (a:A | a:B)",
     1.8 -   "(a : A Int B)  =  (a:A & a:B)",
     1.9 -   "(a : Compl(B)) =  (~a:B)",
    1.10 -   "(a : A-B)      =  (a:A & ~a:B)",
    1.11 + [ "(a : A Un B)   =  (a:A | a:B)",	(* Un_iff *)
    1.12 +   "(a : A Int B)  =  (a:A & a:B)",	(* Int_iff *)
    1.13 +   "(a : Compl(B)) =  (~a:B)",		(* Compl_iff *)
    1.14 +   "(a : A-B)      =  (a:A & ~a:B)",	(* Diff_iff *)
    1.15     "(a : {b})      =  (a=b)",
    1.16     "(a : {x.P(x)}) =  P(a)" ];
    1.17