--- a/src/HOL/Set.thy Fri Dec 13 18:32:07 1996 +0100
+++ b/src/HOL/Set.thy Fri Dec 13 18:40:50 1996 +0100
@@ -127,24 +127,23 @@
Ball_def "Ball A P == ! x. x:A --> P(x)"
Bex_def "Bex A P == ? x. x:A & P(x)"
subset_def "A <= B == ! x:A. x:B"
- Compl_def "Compl(A) == {x. ~x:A}"
+ Compl_def "Compl A == {x. ~x:A}"
Un_def "A Un B == {x.x:A | x:B}"
Int_def "A Int B == {x.x:A & x:B}"
set_diff_def "A - B == {x. x:A & ~x:B}"
INTER_def "INTER A B == {y. ! x:A. y: B(x)}"
UNION_def "UNION A B == {y. ? x:A. y: B(x)}"
- INTER1_def "INTER1(B) == INTER {x.True} B"
- UNION1_def "UNION1(B) == UNION {x.True} B"
- Inter_def "Inter(S) == (INT x:S. x)"
- Union_def "Union(S) == (UN x:S. x)"
- Pow_def "Pow(A) == {B. B <= A}"
+ INTER1_def "INTER1 B == INTER {x.True} B"
+ UNION1_def "UNION1 B == UNION {x.True} B"
+ Inter_def "Inter S == (INT x:S. x)"
+ Union_def "Union S == (UN x:S. x)"
+ Pow_def "Pow A == {B. B <= A}"
empty_def "{} == {x. False}"
insert_def "insert a B == {x.x=a} Un B"
image_def "f``A == {y. ? x:A. y=f(x)}"
- inj_def "inj(f) == ! x y. f(x)=f(y) --> x=y"
+ inj_def "inj f == ! x y. f(x)=f(y) --> x=y"
inj_onto_def "inj_onto f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
- surj_def "surj(f) == ! y. ? x. y=f(x)"
-
+ surj_def "surj f == ! y. ? x. y=f(x)"
end