src/ZF/OrdQuant.thy

--- a/src/ZF/OrdQuant.thy	Tue Jul 16 16:28:26 2002 +0200
+++ b/src/ZF/OrdQuant.thy	Tue Jul 16 16:28:49 2002 +0200
@@ -334,9 +334,10 @@
 subsubsection{*Sets as Classes*}
 
 constdefs setclass :: "[i,i] => o"       ("**_" [40] 40)
-   "setclass(A,x) == x : A"
+   "setclass(A) == %x. x : A"
 
-declare setclass_def [simp]
+lemma setclass_iff [simp]: "setclass(A,x) <-> x : A"
+by (simp add: setclass_def)
 
 lemma rall_setclass_is_ball [simp]: "(\<forall>x[**A]. P(x)) <-> (\<forall>x\<in>A. P(x))"
 by auto