--- a/src/ZF/OrdQuant.thy Wed Feb 05 13:35:32 2003 +0100
+++ b/src/ZF/OrdQuant.thy Thu Feb 06 11:01:05 2003 +0100
@@ -333,16 +333,16 @@
subsubsection{*Sets as Classes*}
-constdefs setclass :: "[i,i] => o" ("**_" [40] 40)
+constdefs setclass :: "[i,i] => o" ("##_" [40] 40)
"setclass(A) == %x. x : A"
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))"
+lemma rall_setclass_is_ball [simp]: "(\<forall>x[##A]. P(x)) <-> (\<forall>x\<in>A. P(x))"
by auto
-lemma rex_setclass_is_bex [simp]: "(\<exists>x[**A]. P(x)) <-> (\<exists>x\<in>A. P(x))"
+lemma rex_setclass_is_bex [simp]: "(\<exists>x[##A]. P(x)) <-> (\<exists>x\<in>A. P(x))"
by auto