--- a/Set.thy Thu Aug 25 10:47:33 1994 +0200
+++ b/Set.thy Thu Aug 25 11:01:45 1994 +0200
@@ -27,6 +27,7 @@
UNION1 :: "['a => 'b set] => 'b set" (binder "UN " 10)
INTER1 :: "['a => 'b set] => 'b set" (binder "INT " 10)
Union, Inter :: "(('a set)set) => 'a set" (*of a set*)
+ Pow :: "'a set => 'a set set" (*powerset*)
range :: "('a => 'b) => 'b set" (*of function*)
Ball, Bex :: "['a set, 'a => bool] => bool" (*bounded quantifiers*)
inj, surj :: "('a => 'b) => bool" (*inj/surjective*)
@@ -80,8 +81,8 @@
mem_Collect_eq "(a : {x.P(x)}) = P(a)"
Collect_mem_eq "{x.x:A} = A"
- (* Definitions *)
+defs
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"
@@ -95,6 +96,7 @@
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"
range_def "range(f) == {y. ? x. y=f(x)}"