--- a/src/HOL/Fun.ML Tue Apr 23 16:44:22 1996 +0200
+++ b/src/HOL/Fun.ML Tue Apr 23 16:58:21 1996 +0200
@@ -186,10 +186,10 @@
fun prover s = prove_goal Fun.thy s (fn _=>[fast_tac set_cs 1]);
val mem_simps = map prover
- [ "(a : A Un B) = (a:A | a:B)",
- "(a : A Int B) = (a:A & a:B)",
- "(a : Compl(B)) = (~a:B)",
- "(a : A-B) = (a:A & ~a:B)",
+ [ "(a : A Un B) = (a:A | a:B)", (* Un_iff *)
+ "(a : A Int B) = (a:A & a:B)", (* Int_iff *)
+ "(a : Compl(B)) = (~a:B)", (* Compl_iff *)
+ "(a : A-B) = (a:A & ~a:B)", (* Diff_iff *)
"(a : {b}) = (a=b)",
"(a : {x.P(x)}) = P(a)" ];