diff -r d9527f97246e -r 89669c58e506 Set.thy
--- 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)}"