diff -r 95f1e700b712 -r 57bf0cecb366 src/ZF/UNITY/State.thy
--- a/src/ZF/UNITY/State.thy	Tue Mar 06 16:46:27 2012 +0000
+++ b/src/ZF/UNITY/State.thy	Tue Mar 06 17:01:37 2012 +0000
@@ -51,19 +51,19 @@
 
 (* Union *)
 
-lemma st_set_Un_iff [iff]: "st_set(A Un B) <-> st_set(A) & st_set(B)"
+lemma st_set_Un_iff [iff]: "st_set(A \<union> B) \<longleftrightarrow> st_set(A) & st_set(B)"
 by (simp add: st_set_def, auto)
 
-lemma st_set_Union_iff [iff]: "st_set(Union(S)) <-> (\<forall>A \<in> S. st_set(A))"
+lemma st_set_Union_iff [iff]: "st_set(\<Union>(S)) \<longleftrightarrow> (\<forall>A \<in> S. st_set(A))"
 by (simp add: st_set_def, auto)
 
 (* Intersection *)
 
-lemma st_set_Int [intro!]: "st_set(A) | st_set(B) ==> st_set(A Int B)"
+lemma st_set_Int [intro!]: "st_set(A) | st_set(B) ==> st_set(A \<inter> B)"
 by (simp add: st_set_def, auto)
 
 lemma st_set_Inter [intro!]: 
-   "(S=0) | (\<exists>A \<in> S. st_set(A)) ==> st_set(Inter(S))"
+   "(S=0) | (\<exists>A \<in> S. st_set(A)) ==> st_set(\<Inter>(S))"
 apply (simp add: st_set_def Inter_def, auto)
 done
 
@@ -71,16 +71,16 @@
 lemma st_set_DiffI [intro!]: "st_set(A) ==> st_set(A - B)"
 by (simp add: st_set_def, auto)
 
-lemma Collect_Int_state [simp]: "Collect(state,P) Int state = Collect(state,P)"
+lemma Collect_Int_state [simp]: "Collect(state,P) \<inter> state = Collect(state,P)"
 by auto
 
-lemma state_Int_Collect [simp]: "state Int Collect(state,P) = Collect(state,P)"
+lemma state_Int_Collect [simp]: "state \<inter> Collect(state,P) = Collect(state,P)"
 by auto
 
 
 (* Introduction and destruction rules for st_set *)
 
-lemma st_setI: "A <= state ==> st_set(A)"
+lemma st_setI: "A \<subseteq> state ==> st_set(A)"
 by (simp add: st_set_def)
 
 lemma st_setD: "st_set(A) ==> A<=state"
@@ -99,7 +99,7 @@
 lemma st_set_compl [simp]: "st_set(st_compl(A))"
 by (simp add: st_compl_def, auto)
 
-lemma st_compl_iff [simp]: "x \<in> st_compl(A) <-> x \<in> state & x \<notin> A"
+lemma st_compl_iff [simp]: "x \<in> st_compl(A) \<longleftrightarrow> x \<in> state & x \<notin> A"
 by (simp add: st_compl_def)
 
 lemma st_compl_Collect [simp]: