# HG changeset patch
# User paulson
# Date 1331050012 0
# Node ID ff6b0c1087f27dc8b7dcda7384a3439e65dd456c
# Parent  c656222c4dc12adbfc847e9ff471134875d3c807
Using mathematical notation for <-> and cardinal arithmetic

diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/Arith.thy
--- a/src/ZF/Arith.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Arith.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -311,7 +311,7 @@
 lemma add_lt_elim1: "[| k#+m < k#+n; m \<in> nat; n \<in> nat |] ==> m < n"
 by (drule add_lt_elim1_natify, auto)
 
-lemma zero_less_add: "[| n \<in> nat; m \<in> nat |] ==> 0 < m #+ n <-> (0<m | 0<n)"
+lemma zero_less_add: "[| n \<in> nat; m \<in> nat |] ==> 0 < m #+ n \<longleftrightarrow> (0<m | 0<n)"
 by (induct_tac "n", auto)
 
 
@@ -441,13 +441,13 @@
 
 (** Lemmas for the CancelNumerals simproc **)
 
-lemma eq_add_iff: "(u #+ m = u #+ n) <-> (0 #+ m = natify(n))"
+lemma eq_add_iff: "(u #+ m = u #+ n) \<longleftrightarrow> (0 #+ m = natify(n))"
 apply auto
 apply (blast dest: add_left_cancel_natify)
 apply (simp add: add_def)
 done
 
-lemma less_add_iff: "(u #+ m < u #+ n) <-> (0 #+ m < natify(n))"
+lemma less_add_iff: "(u #+ m < u #+ n) \<longleftrightarrow> (0 #+ m < natify(n))"
 apply (auto simp add: add_lt_elim1_natify)
 apply (drule add_lt_mono1)
 apply (auto simp add: add_commute [of u])
@@ -460,7 +460,7 @@
 lemma eq_cong2: "u = u' ==> (t==u) == (t==u')"
 by auto
 
-lemma iff_cong2: "u <-> u' ==> (t==u) == (t==u')"
+lemma iff_cong2: "u \<longleftrightarrow> u' ==> (t==u) == (t==u')"
 by auto
 
 
@@ -543,11 +543,11 @@
 
 lemma lt_succ_eq_0_disj:
      "[| m\<in>nat; n\<in>nat |]
-      ==> (m < succ(n)) <-> (m = 0 | (\<exists>j\<in>nat. m = succ(j) & j < n))"
+      ==> (m < succ(n)) \<longleftrightarrow> (m = 0 | (\<exists>j\<in>nat. m = succ(j) & j < n))"
 by (induct_tac "m", auto)
 
 lemma less_diff_conv [rule_format]:
-     "[| j\<in>nat; k\<in>nat |] ==> \<forall>i\<in>nat. (i < j #- k) <-> (i #+ k < j)"
+     "[| j\<in>nat; k\<in>nat |] ==> \<forall>i\<in>nat. (i < j #- k) \<longleftrightarrow> (i #+ k < j)"
 by (erule_tac m = k in diff_induct, auto)
 
 lemmas nat_typechecks = rec_type nat_0I nat_1I nat_succI Ord_nat
diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/ArithSimp.thy
--- a/src/ZF/ArithSimp.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/ArithSimp.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -43,7 +43,7 @@
 done
 
 lemma zero_less_diff [simp]:
-     "[| m: nat; n: nat |] ==> 0 < (n #- m)   <->   m<n"
+     "[| m: nat; n: nat |] ==> 0 < (n #- m)   \<longleftrightarrow>   m<n"
 apply (rule_tac m = m and n = n in diff_induct)
 apply (simp_all (no_asm_simp))
 done
@@ -301,37 +301,37 @@
 apply (simp (no_asm_simp) add: mult_lt_mono2 mult_commute [of _ k])
 done
 
-lemma add_eq_0_iff [iff]: "m#+n = 0 <-> natify(m)=0 & natify(n)=0"
-apply (subgoal_tac "natify (m) #+ natify (n) = 0 <-> natify (m) =0 & natify (n) =0")
+lemma add_eq_0_iff [iff]: "m#+n = 0 \<longleftrightarrow> natify(m)=0 & natify(n)=0"
+apply (subgoal_tac "natify (m) #+ natify (n) = 0 \<longleftrightarrow> natify (m) =0 & natify (n) =0")
 apply (rule_tac [2] n = "natify (m) " in natE)
  apply (rule_tac [4] n = "natify (n) " in natE)
 apply auto
 done
 
-lemma zero_lt_mult_iff [iff]: "0 < m#*n <-> 0 < natify(m) & 0 < natify(n)"
-apply (subgoal_tac "0 < natify (m) #*natify (n) <-> 0 < natify (m) & 0 < natify (n) ")
+lemma zero_lt_mult_iff [iff]: "0 < m#*n \<longleftrightarrow> 0 < natify(m) & 0 < natify(n)"
+apply (subgoal_tac "0 < natify (m) #*natify (n) \<longleftrightarrow> 0 < natify (m) & 0 < natify (n) ")
 apply (rule_tac [2] n = "natify (m) " in natE)
  apply (rule_tac [4] n = "natify (n) " in natE)
   apply (rule_tac [3] n = "natify (n) " in natE)
 apply auto
 done
 
-lemma mult_eq_1_iff [iff]: "m#*n = 1 <-> natify(m)=1 & natify(n)=1"
-apply (subgoal_tac "natify (m) #* natify (n) = 1 <-> natify (m) =1 & natify (n) =1")
+lemma mult_eq_1_iff [iff]: "m#*n = 1 \<longleftrightarrow> natify(m)=1 & natify(n)=1"
+apply (subgoal_tac "natify (m) #* natify (n) = 1 \<longleftrightarrow> natify (m) =1 & natify (n) =1")
 apply (rule_tac [2] n = "natify (m) " in natE)
  apply (rule_tac [4] n = "natify (n) " in natE)
 apply auto
 done
 
 
-lemma mult_is_zero: "[|m: nat; n: nat|] ==> (m #* n = 0) <-> (m = 0 | n = 0)"
+lemma mult_is_zero: "[|m: nat; n: nat|] ==> (m #* n = 0) \<longleftrightarrow> (m = 0 | n = 0)"
 apply auto
 apply (erule natE)
 apply (erule_tac [2] natE, auto)
 done
 
 lemma mult_is_zero_natify [iff]:
-     "(m #* n = 0) <-> (natify(m) = 0 | natify(n) = 0)"
+     "(m #* n = 0) \<longleftrightarrow> (natify(m) = 0 | natify(n) = 0)"
 apply (cut_tac m = "natify (m) " and n = "natify (n) " in mult_is_zero)
 apply auto
 done
@@ -340,7 +340,7 @@
 subsection{*Cancellation Laws for Common Factors in Comparisons*}
 
 lemma mult_less_cancel_lemma:
-     "[| k: nat; m: nat; n: nat |] ==> (m#*k < n#*k) <-> (0<k & m<n)"
+     "[| k: nat; m: nat; n: nat |] ==> (m#*k < n#*k) \<longleftrightarrow> (0<k & m<n)"
 apply (safe intro!: mult_lt_mono1)
 apply (erule natE, auto)
 apply (rule not_le_iff_lt [THEN iffD1])
@@ -349,22 +349,22 @@
 done
 
 lemma mult_less_cancel2 [simp]:
-     "(m#*k < n#*k) <-> (0 < natify(k) & natify(m) < natify(n))"
+     "(m#*k < n#*k) \<longleftrightarrow> (0 < natify(k) & natify(m) < natify(n))"
 apply (rule iff_trans)
 apply (rule_tac [2] mult_less_cancel_lemma, auto)
 done
 
 lemma mult_less_cancel1 [simp]:
-     "(k#*m < k#*n) <-> (0 < natify(k) & natify(m) < natify(n))"
+     "(k#*m < k#*n) \<longleftrightarrow> (0 < natify(k) & natify(m) < natify(n))"
 apply (simp (no_asm) add: mult_less_cancel2 mult_commute [of k])
 done
 
-lemma mult_le_cancel2 [simp]: "(m#*k \<le> n#*k) <-> (0 < natify(k) \<longrightarrow> natify(m) \<le> natify(n))"
+lemma mult_le_cancel2 [simp]: "(m#*k \<le> n#*k) \<longleftrightarrow> (0 < natify(k) \<longrightarrow> natify(m) \<le> natify(n))"
 apply (simp (no_asm_simp) add: not_lt_iff_le [THEN iff_sym])
 apply auto
 done
 
-lemma mult_le_cancel1 [simp]: "(k#*m \<le> k#*n) <-> (0 < natify(k) \<longrightarrow> natify(m) \<le> natify(n))"
+lemma mult_le_cancel1 [simp]: "(k#*m \<le> k#*n) \<longleftrightarrow> (0 < natify(k) \<longrightarrow> natify(m) \<le> natify(n))"
 apply (simp (no_asm_simp) add: not_lt_iff_le [THEN iff_sym])
 apply auto
 done
@@ -372,23 +372,23 @@
 lemma mult_le_cancel_le1: "k \<in> nat ==> k #* m \<le> k \<longleftrightarrow> (0 < k \<longrightarrow> natify(m) \<le> 1)"
 by (cut_tac k = k and m = m and n = 1 in mult_le_cancel1, auto)
 
-lemma Ord_eq_iff_le: "[| Ord(m); Ord(n) |] ==> m=n <-> (m \<le> n & n \<le> m)"
+lemma Ord_eq_iff_le: "[| Ord(m); Ord(n) |] ==> m=n \<longleftrightarrow> (m \<le> n & n \<le> m)"
 by (blast intro: le_anti_sym)
 
 lemma mult_cancel2_lemma:
-     "[| k: nat; m: nat; n: nat |] ==> (m#*k = n#*k) <-> (m=n | k=0)"
+     "[| k: nat; m: nat; n: nat |] ==> (m#*k = n#*k) \<longleftrightarrow> (m=n | k=0)"
 apply (simp (no_asm_simp) add: Ord_eq_iff_le [of "m#*k"] Ord_eq_iff_le [of m])
 apply (auto simp add: Ord_0_lt_iff)
 done
 
 lemma mult_cancel2 [simp]:
-     "(m#*k = n#*k) <-> (natify(m) = natify(n) | natify(k) = 0)"
+     "(m#*k = n#*k) \<longleftrightarrow> (natify(m) = natify(n) | natify(k) = 0)"
 apply (rule iff_trans)
 apply (rule_tac [2] mult_cancel2_lemma, auto)
 done
 
 lemma mult_cancel1 [simp]:
-     "(k#*m = k#*n) <-> (natify(m) = natify(n) | natify(k) = 0)"
+     "(k#*m = k#*n) \<longleftrightarrow> (natify(m) = natify(n) | natify(k) = 0)"
 apply (simp (no_asm) add: mult_cancel2 mult_commute [of k])
 done
 
@@ -493,7 +493,7 @@
 done
 
 lemma less_iff_succ_add:
-     "[| m: nat; n: nat |] ==> (m<n) <-> (\<exists>k\<in>nat. n = succ(m#+k))"
+     "[| m: nat; n: nat |] ==> (m<n) \<longleftrightarrow> (\<exists>k\<in>nat. n = succ(m#+k))"
 by (auto intro: less_imp_succ_add)
 
 lemma add_lt_elim2:
@@ -508,11 +508,11 @@
 subsubsection{*More Lemmas About Difference*}
 
 lemma diff_is_0_lemma:
-     "[| m: nat; n: nat |] ==> m #- n = 0 <-> m \<le> n"
+     "[| m: nat; n: nat |] ==> m #- n = 0 \<longleftrightarrow> m \<le> n"
 apply (rule_tac m = m and n = n in diff_induct, simp_all)
 done
 
-lemma diff_is_0_iff: "m #- n = 0 <-> natify(m) \<le> natify(n)"
+lemma diff_is_0_iff: "m #- n = 0 \<longleftrightarrow> natify(m) \<le> natify(n)"
 by (simp add: diff_is_0_lemma [symmetric])
 
 lemma nat_lt_imp_diff_eq_0:
@@ -521,7 +521,7 @@
 
 lemma raw_nat_diff_split:
      "[| a:nat; b:nat |] ==>
-      (P(a #- b)) <-> ((a < b \<longrightarrow>P(0)) & (\<forall>d\<in>nat. a = b #+ d \<longrightarrow> P(d)))"
+      (P(a #- b)) \<longleftrightarrow> ((a < b \<longrightarrow>P(0)) & (\<forall>d\<in>nat. a = b #+ d \<longrightarrow> P(d)))"
 apply (case_tac "a < b")
  apply (force simp add: nat_lt_imp_diff_eq_0)
 apply (rule iffI, force, simp)
@@ -530,7 +530,7 @@
 done
 
 lemma nat_diff_split:
-   "(P(a #- b)) <->
+   "(P(a #- b)) \<longleftrightarrow>
     (natify(a) < natify(b) \<longrightarrow>P(0)) & (\<forall>d\<in>nat. natify(a) = b #+ d \<longrightarrow> P(d))"
 apply (cut_tac P=P and a="natify(a)" and b="natify(b)" in raw_nat_diff_split)
 apply simp_all
@@ -559,7 +559,7 @@
 done
 
 
-lemma diff_lt_iff_lt: "[|i\<le>k; j\<in>nat; k\<in>nat|] ==> (k#-i) < (k#-j) <-> j<i"
+lemma diff_lt_iff_lt: "[|i\<le>k; j\<in>nat; k\<in>nat|] ==> (k#-i) < (k#-j) \<longleftrightarrow> j<i"
 apply (frule le_in_nat, assumption)
 apply (blast intro: lt_imp_diff_lt diff_lt_imp_lt)
 done
diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/Bin.thy
--- a/src/ZF/Bin.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Bin.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -346,7 +346,7 @@
 
 lemma eq_integ_of_eq:
      "[| v: bin;  w: bin |]
-      ==> ((integ_of(v)) = integ_of(w)) <->
+      ==> ((integ_of(v)) = integ_of(w)) \<longleftrightarrow>
           iszero (integ_of (bin_add (v, bin_minus(w))))"
 apply (unfold iszero_def)
 apply (simp add: zcompare_rls integ_of_add integ_of_minus)
@@ -363,7 +363,7 @@
 
 lemma iszero_integ_of_BIT:
      "[| w: bin; x: bool |]
-      ==> iszero (integ_of (w BIT x)) <-> (x=0 & iszero (integ_of(w)))"
+      ==> iszero (integ_of (w BIT x)) \<longleftrightarrow> (x=0 & iszero (integ_of(w)))"
 apply (unfold iszero_def, simp)
 apply (subgoal_tac "integ_of (w) \<in> int")
 apply typecheck
@@ -374,7 +374,7 @@
 done
 
 lemma iszero_integ_of_0:
-     "w: bin ==> iszero (integ_of (w BIT 0)) <-> iszero (integ_of(w))"
+     "w: bin ==> iszero (integ_of (w BIT 0)) \<longleftrightarrow> iszero (integ_of(w))"
 by (simp only: iszero_integ_of_BIT, blast)
 
 lemma iszero_integ_of_1: "w: bin ==> ~ iszero (integ_of (w BIT 1))"
@@ -387,7 +387,7 @@
 lemma less_integ_of_eq_neg:
      "[| v: bin;  w: bin |]
       ==> integ_of(v) $< integ_of(w)
-          <-> znegative (integ_of (bin_add (v, bin_minus(w))))"
+          \<longleftrightarrow> znegative (integ_of (bin_add (v, bin_minus(w))))"
 apply (unfold zless_def zdiff_def)
 apply (simp add: integ_of_minus integ_of_add)
 done
@@ -400,7 +400,7 @@
 
 lemma neg_integ_of_BIT:
      "[| w: bin; x: bool |]
-      ==> znegative (integ_of (w BIT x)) <-> znegative (integ_of(w))"
+      ==> znegative (integ_of (w BIT x)) \<longleftrightarrow> znegative (integ_of(w))"
 apply simp
 apply (subgoal_tac "integ_of (w) \<in> int")
 apply typecheck
@@ -416,7 +416,7 @@
 (** Less-than-or-equals (<=) **)
 
 lemma le_integ_of_eq_not_less:
-     "(integ_of(x) $<= (integ_of(w))) <-> ~ (integ_of(w) $< (integ_of(x)))"
+     "(integ_of(x) $<= (integ_of(w))) \<longleftrightarrow> ~ (integ_of(w) $< (integ_of(x)))"
 by (simp add: not_zless_iff_zle [THEN iff_sym])
 
 
@@ -509,7 +509,7 @@
 lemma zdiff_self [simp]: "x $- x = #0"
 by (simp add: zdiff_def)
 
-lemma znegative_iff_zless_0: "k: int ==> znegative(k) <-> k $< #0"
+lemma znegative_iff_zless_0: "k: int ==> znegative(k) \<longleftrightarrow> k $< #0"
 by (simp add: zless_def)
 
 lemma zero_zless_imp_znegative_zminus: "[|#0 $< k; k: int|] ==> znegative($-k)"
@@ -545,7 +545,7 @@
 lemma int_of_nat_of_if: "$# nat_of(z) = (if #0 $<= z then intify(z) else #0)"
 by (simp add: int_of_nat_of znegative_iff_zless_0 not_zle_iff_zless)
 
-lemma zless_nat_iff_int_zless: "[| m: nat; z: int |] ==> (m < nat_of(z)) <-> ($#m $< z)"
+lemma zless_nat_iff_int_zless: "[| m: nat; z: int |] ==> (m < nat_of(z)) \<longleftrightarrow> ($#m $< z)"
 apply (case_tac "znegative (z) ")
 apply (erule_tac [2] not_zneg_nat_of [THEN subst])
 apply (auto dest: zless_trans dest!: zero_zle_int_of [THEN zle_zless_trans]
@@ -556,7 +556,7 @@
 (** nat_of and zless **)
 
 (*An alternative condition is  @{term"$#0 \<subseteq> w"}  *)
-lemma zless_nat_conj_lemma: "$#0 $< z ==> (nat_of(w) < nat_of(z)) <-> (w $< z)"
+lemma zless_nat_conj_lemma: "$#0 $< z ==> (nat_of(w) < nat_of(z)) \<longleftrightarrow> (w $< z)"
 apply (rule iff_trans)
 apply (rule zless_int_of [THEN iff_sym])
 apply (auto simp add: int_of_nat_of_if simp del: zless_int_of)
@@ -564,7 +564,7 @@
 apply (blast intro: zless_zle_trans)
 done
 
-lemma zless_nat_conj: "(nat_of(w) < nat_of(z)) <-> ($#0 $< z & w $< z)"
+lemma zless_nat_conj: "(nat_of(w) < nat_of(z)) \<longleftrightarrow> ($#0 $< z & w $< z)"
 apply (case_tac "$#0 $< z")
 apply (auto simp add: zless_nat_conj_lemma nat_le_int0 not_zless_iff_zle)
 done
@@ -575,24 +575,24 @@
     Conditional rewrite rules are tried after unconditional ones, so a rule
     like eq_nat_number_of will be tried first to eliminate #mm=#nn.]
   lemma integ_of_reorient [simp]:
-       "True ==> (integ_of(w) = x) <-> (x = integ_of(w))"
+       "True ==> (integ_of(w) = x) \<longleftrightarrow> (x = integ_of(w))"
   by auto
 *)
 
 lemma integ_of_minus_reorient [simp]:
-     "(integ_of(w) = $- x) <-> ($- x = integ_of(w))"
+     "(integ_of(w) = $- x) \<longleftrightarrow> ($- x = integ_of(w))"
 by auto
 
 lemma integ_of_add_reorient [simp]:
-     "(integ_of(w) = x $+ y) <-> (x $+ y = integ_of(w))"
+     "(integ_of(w) = x $+ y) \<longleftrightarrow> (x $+ y = integ_of(w))"
 by auto
 
 lemma integ_of_diff_reorient [simp]:
-     "(integ_of(w) = x $- y) <-> (x $- y = integ_of(w))"
+     "(integ_of(w) = x $- y) \<longleftrightarrow> (x $- y = integ_of(w))"
 by auto
 
 lemma integ_of_mult_reorient [simp]:
-     "(integ_of(w) = x $* y) <-> (x $* y = integ_of(w))"
+     "(integ_of(w) = x $* y) \<longleftrightarrow> (x $* y = integ_of(w))"
 by auto
 
 end
diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/Bool.thy
--- a/src/ZF/Bool.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Bool.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -164,10 +164,10 @@
 lemma [simp,TC]: "bool_of_o(P) \<in> bool"
 by (simp add: bool_of_o_def)
 
-lemma [simp]: "(bool_of_o(P) = 1) <-> P"
+lemma [simp]: "(bool_of_o(P) = 1) \<longleftrightarrow> P"
 by (simp add: bool_of_o_def)
 
-lemma [simp]: "(bool_of_o(P) = 0) <-> ~P"
+lemma [simp]: "(bool_of_o(P) = 0) \<longleftrightarrow> ~P"
 by (simp add: bool_of_o_def)
 
 end
diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/Cardinal.thy
--- a/src/ZF/Cardinal.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Cardinal.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -138,7 +138,7 @@
     "[| X \<approx> Y; [| X \<lesssim> Y; Y \<lesssim> X |] ==> P |] ==> P"
 by (blast intro: eqpoll_imp_lepoll eqpoll_sym)
 
-lemma eqpoll_iff: "X \<approx> Y <-> X \<lesssim> Y & Y \<lesssim> X"
+lemma eqpoll_iff: "X \<approx> Y \<longleftrightarrow> X \<lesssim> Y & Y \<lesssim> X"
 by (blast intro: eqpollI elim!: eqpollE)
 
 lemma lepoll_0_is_0: "A \<lesssim> 0 ==> A = 0"
@@ -149,7 +149,7 @@
 (*@{term"0 \<lesssim> Y"}*)
 lemmas empty_lepollI = empty_subsetI [THEN subset_imp_lepoll]
 
-lemma lepoll_0_iff: "A \<lesssim> 0 <-> A=0"
+lemma lepoll_0_iff: "A \<lesssim> 0 \<longleftrightarrow> A=0"
 by (blast intro: lepoll_0_is_0 lepoll_refl)
 
 lemma Un_lepoll_Un:
@@ -161,7 +161,7 @@
 (*A eqpoll 0 ==> A=0*)
 lemmas eqpoll_0_is_0 = eqpoll_imp_lepoll [THEN lepoll_0_is_0]
 
-lemma eqpoll_0_iff: "A \<approx> 0 <-> A=0"
+lemma eqpoll_0_iff: "A \<approx> 0 \<longleftrightarrow> A=0"
 by (blast intro: eqpoll_0_is_0 eqpoll_refl)
 
 lemma eqpoll_disjoint_Un:
@@ -188,7 +188,7 @@
 apply (blast intro: well_ord_rvimage)
 done
 
-lemma lepoll_iff_leqpoll: "A \<lesssim> B <-> A \<prec> B | A \<approx> B"
+lemma lepoll_iff_leqpoll: "A \<lesssim> B \<longleftrightarrow> A \<prec> B | A \<approx> B"
 apply (unfold lesspoll_def)
 apply (blast intro!: eqpollI elim!: eqpollE)
 done
@@ -288,7 +288,7 @@
 
 (*Not needed for simplification, but helpful below*)
 lemma Least_cong:
-     "(!!y. P(y) <-> Q(y)) ==> (LEAST x. P(x)) = (LEAST x. Q(x))"
+     "(!!y. P(y) \<longleftrightarrow> Q(y)) ==> (LEAST x. P(x)) = (LEAST x. Q(x))"
 by simp
 
 (*Need AC to get @{term"X \<lesssim> Y ==> |X| \<le> |Y|"};  see well_ord_lepoll_imp_Card_le
@@ -319,7 +319,7 @@
 done
 
 lemma well_ord_cardinal_eqpoll_iff:
-     "[| well_ord(X,r);  well_ord(Y,s) |] ==> |X| = |Y| <-> X \<approx> Y"
+     "[| well_ord(X,r);  well_ord(Y,s) |] ==> |X| = |Y| \<longleftrightarrow> X \<approx> Y"
 by (blast intro: cardinal_cong well_ord_cardinal_eqE)
 
 
@@ -358,7 +358,7 @@
 done
 
 (*The cardinals are the initial ordinals*)
-lemma Card_iff_initial: "Card(K) <-> Ord(K) & (\<forall>j. j<K \<longrightarrow> ~ j \<approx> K)"
+lemma Card_iff_initial: "Card(K) \<longleftrightarrow> Ord(K) & (\<forall>j. j<K \<longrightarrow> ~ j \<approx> K)"
 apply (safe intro!: CardI Card_is_Ord)
  prefer 2 apply blast
 apply (unfold Card_def cardinal_def)
@@ -430,10 +430,10 @@
 apply (simp (no_asm_simp) add: cardinal_lt_imp_lt Card_is_Ord Card_cardinal_eq)
 done
 
-lemma Card_lt_iff: "[| Ord(i);  Card(K) |] ==> (|i| < K) <-> (i < K)"
+lemma Card_lt_iff: "[| Ord(i);  Card(K) |] ==> (|i| < K) \<longleftrightarrow> (i < K)"
 by (blast intro: Card_lt_imp_lt Ord_cardinal_le [THEN lt_trans1])
 
-lemma Card_le_iff: "[| Ord(i);  Card(K) |] ==> (K \<le> |i|) <-> (K \<le> i)"
+lemma Card_le_iff: "[| Ord(i);  Card(K) |] ==> (K \<le> |i|) \<longleftrightarrow> (K \<le> i)"
 by (simp add: Card_lt_iff Card_is_Ord Ord_cardinal not_lt_iff_le [THEN iff_sym])
 
 (*Can use AC or finiteness to discharge first premise*)
@@ -510,7 +510,7 @@
 apply (blast intro!: succ_leI dest!: succ_lepoll_succD)
 done
 
-lemma nat_eqpoll_iff: "[| m:nat; n: nat |] ==> m \<approx> n <-> m = n"
+lemma nat_eqpoll_iff: "[| m:nat; n: nat |] ==> m \<approx> n \<longleftrightarrow> m = n"
 apply (rule iffI)
 apply (blast intro: nat_lepoll_imp_le le_anti_sym elim!: eqpollE)
 apply (simp add: eqpoll_refl)
@@ -573,7 +573,7 @@
 apply (blast intro!: inj_not_surj_succ)
 done
 
-lemma lesspoll_succ_iff: "m:nat ==> A \<prec> succ(m) <-> A \<lesssim> m"
+lemma lesspoll_succ_iff: "m:nat ==> A \<prec> succ(m) \<longleftrightarrow> A \<lesssim> m"
 by (blast intro!: lepoll_imp_lesspoll_succ lesspoll_succ_imp_lepoll)
 
 lemma lepoll_succ_disj: "[| A \<lesssim> succ(m);  m:nat |] ==> A \<lesssim> m | A \<approx> succ(m)"
@@ -602,7 +602,7 @@
 apply (rule Ord_succ_subsetI [THEN subset_imp_lepoll], assumption+)
 done
 
-lemma Ord_nat_eqpoll_iff: "[| Ord(i);  n:nat |] ==> i \<approx> n <-> i=n"
+lemma Ord_nat_eqpoll_iff: "[| Ord(i);  n:nat |] ==> i \<approx> n \<longleftrightarrow> i=n"
 apply (rule iffI)
  prefer 2 apply (simp add: eqpoll_refl)
 apply (rule Ord_linear_lt [of i n])
@@ -647,11 +647,11 @@
 by (simp add: eqpoll_iff cons_lepoll_cong)
 
 lemma cons_lepoll_cons_iff:
-     "[| a \<notin> A;  b \<notin> B |] ==> cons(a,A) \<lesssim> cons(b,B)  <->  A \<lesssim> B"
+     "[| a \<notin> A;  b \<notin> B |] ==> cons(a,A) \<lesssim> cons(b,B)  \<longleftrightarrow>  A \<lesssim> B"
 by (blast intro: cons_lepoll_cong cons_lepoll_consD)
 
 lemma cons_eqpoll_cons_iff:
-     "[| a \<notin> A;  b \<notin> B |] ==> cons(a,A) \<approx> cons(b,B)  <->  A \<approx> B"
+     "[| a \<notin> A;  b \<notin> B |] ==> cons(a,A) \<approx> cons(b,B)  \<longleftrightarrow>  A \<approx> B"
 by (blast intro: cons_eqpoll_cong cons_eqpoll_consD)
 
 lemma singleton_eqpoll_1: "{a} \<approx> 1"
@@ -813,10 +813,10 @@
 apply (erule Finite_cons)
 done
 
-lemma Finite_cons_iff [iff]: "Finite(cons(y,x)) <-> Finite(x)"
+lemma Finite_cons_iff [iff]: "Finite(cons(y,x)) \<longleftrightarrow> Finite(x)"
 by (blast intro: Finite_cons subset_Finite)
 
-lemma Finite_succ_iff [iff]: "Finite(succ(x)) <-> Finite(x)"
+lemma Finite_succ_iff [iff]: "Finite(succ(x)) \<longleftrightarrow> Finite(x)"
 by (simp add: succ_def)
 
 lemma nat_le_infinite_Ord:
@@ -859,7 +859,7 @@
 lemma Finite_Fin: "[| Finite(A); A \<subseteq> X |] ==> A \<in> Fin(X)"
 by (unfold Finite_def, blast intro: Finite_Fin_lemma)
 
-lemma eqpoll_imp_Finite_iff: "A \<approx> B ==> Finite(A) <-> Finite(B)"
+lemma eqpoll_imp_Finite_iff: "A \<approx> B ==> Finite(A) \<longleftrightarrow> Finite(B)"
 apply (unfold Finite_def)
 apply (blast intro: eqpoll_trans eqpoll_sym)
 done
@@ -888,7 +888,7 @@
 lemma Fin_into_Finite: "A \<in> Fin(U) ==> Finite(A)"
 by (fast intro!: Finite_0 Finite_cons elim: Fin_induct)
 
-lemma Finite_Fin_iff: "Finite(A) <-> A \<in> Fin(A)"
+lemma Finite_Fin_iff: "Finite(A) \<longleftrightarrow> A \<in> Fin(A)"
 by (blast intro: Finite_into_Fin Fin_into_Finite)
 
 lemma Finite_Un: "[| Finite(A); Finite(B) |] ==> Finite(A \<union> B)"
@@ -897,7 +897,7 @@
           intro: Un_upper1 [THEN Fin_mono, THEN subsetD]
                  Un_upper2 [THEN Fin_mono, THEN subsetD])
 
-lemma Finite_Un_iff [simp]: "Finite(A \<union> B) <-> (Finite(A) & Finite(B))"
+lemma Finite_Un_iff [simp]: "Finite(A \<union> B) \<longleftrightarrow> (Finite(A) & Finite(B))"
 by (blast intro: subset_Finite Finite_Un)
 
 text{*The converse must hold too.*}
@@ -961,7 +961,7 @@
 text{*I don't know why, but if the premise is expressed using meta-connectives
 then  the simplifier cannot prove it automatically in conditional rewriting.*}
 lemma Finite_RepFun_iff:
-     "(\<forall>x y. f(x)=f(y) \<longrightarrow> x=y) ==> Finite(RepFun(A,f)) <-> Finite(A)"
+     "(\<forall>x y. f(x)=f(y) \<longrightarrow> x=y) ==> Finite(RepFun(A,f)) \<longleftrightarrow> Finite(A)"
 by (blast intro: Finite_RepFun Finite_RepFun_iff_lemma [of _ f])
 
 lemma Finite_Pow: "Finite(A) ==> Finite(Pow(A))"
@@ -975,7 +975,7 @@
 apply (blast intro: subset_Finite)
 done
 
-lemma Finite_Pow_iff [iff]: "Finite(Pow(A)) <-> Finite(A)"
+lemma Finite_Pow_iff [iff]: "Finite(Pow(A)) \<longleftrightarrow> Finite(A)"
 by (blast intro: Finite_Pow Finite_Pow_imp_Finite)
 
 
diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/CardinalArith.thy
--- a/src/ZF/CardinalArith.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/CardinalArith.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -39,11 +39,11 @@
         of @{term K}*}
     "csucc(K) == LEAST L. Card(L) & K<L"
 
-notation (xsymbols output)
+notation (xsymbols)
   cadd  (infixl "\<oplus>" 65) and
   cmult  (infixl "\<otimes>" 70)
 
-notation (HTML output)
+notation (HTML)
   cadd  (infixl "\<oplus>" 65) and
   cmult  (infixl "\<otimes>" 70)
 
@@ -109,7 +109,7 @@
 apply auto
 done
 
-lemma cadd_commute: "i |+| j = j |+| i"
+lemma cadd_commute: "i \<oplus> j = j \<oplus> i"
 apply (unfold cadd_def)
 apply (rule sum_commute_eqpoll [THEN cardinal_cong])
 done
@@ -125,7 +125,7 @@
 (*Unconditional version requires AC*)
 lemma well_ord_cadd_assoc:
     "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |]
-     ==> (i |+| j) |+| k = i |+| (j |+| k)"
+     ==> (i \<oplus> j) \<oplus> k = i \<oplus> (j \<oplus> k)"
 apply (unfold cadd_def)
 apply (rule cardinal_cong)
 apply (rule eqpoll_trans)
@@ -145,7 +145,7 @@
 apply (rule bij_0_sum)
 done
 
-lemma cadd_0 [simp]: "Card(K) ==> 0 |+| K = K"
+lemma cadd_0 [simp]: "Card(K) ==> 0 \<oplus> K = K"
 apply (unfold cadd_def)
 apply (simp add: sum_0_eqpoll [THEN cardinal_cong] Card_cardinal_eq)
 done
@@ -161,7 +161,7 @@
 (*Could probably weaken the premises to well_ord(K,r), or removing using AC*)
 
 lemma cadd_le_self:
-    "[| Card(K);  Ord(L) |] ==> K \<le> (K |+| L)"
+    "[| Card(K);  Ord(L) |] ==> K \<le> (K \<oplus> L)"
 apply (unfold cadd_def)
 apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le],
        assumption)
@@ -182,7 +182,7 @@
 done
 
 lemma cadd_le_mono:
-    "[| K' \<le> K;  L' \<le> L |] ==> (K' |+| L') \<le> (K |+| L)"
+    "[| K' \<le> K;  L' \<le> L |] ==> (K' \<oplus> L') \<le> (K \<oplus> L)"
 apply (unfold cadd_def)
 apply (safe dest!: le_subset_iff [THEN iffD1])
 apply (rule well_ord_lepoll_imp_Card_le)
@@ -204,7 +204,7 @@
 (*Pulling the  succ(...)  outside the |...| requires m, n: nat  *)
 (*Unconditional version requires AC*)
 lemma cadd_succ_lemma:
-    "[| Ord(m);  Ord(n) |] ==> succ(m) |+| n = |succ(m |+| n)|"
+    "[| Ord(m);  Ord(n) |] ==> succ(m) \<oplus> n = |succ(m \<oplus> n)|"
 apply (unfold cadd_def)
 apply (rule sum_succ_eqpoll [THEN cardinal_cong, THEN trans])
 apply (rule succ_eqpoll_cong [THEN cardinal_cong])
@@ -212,7 +212,7 @@
 apply (blast intro: well_ord_radd well_ord_Memrel)
 done
 
-lemma nat_cadd_eq_add: "[| m: nat;  n: nat |] ==> m |+| n = m#+n"
+lemma nat_cadd_eq_add: "[| m: nat;  n: nat |] ==> m \<oplus> n = m#+n"
 apply (induct_tac m)
 apply (simp add: nat_into_Card [THEN cadd_0])
 apply (simp add: cadd_succ_lemma nat_into_Card [THEN Card_cardinal_eq])
@@ -231,7 +231,7 @@
        auto)
 done
 
-lemma cmult_commute: "i |*| j = j |*| i"
+lemma cmult_commute: "i \<otimes> j = j \<otimes> i"
 apply (unfold cmult_def)
 apply (rule prod_commute_eqpoll [THEN cardinal_cong])
 done
@@ -247,7 +247,7 @@
 (*Unconditional version requires AC*)
 lemma well_ord_cmult_assoc:
     "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |]
-     ==> (i |*| j) |*| k = i |*| (j |*| k)"
+     ==> (i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
 apply (unfold cmult_def)
 apply (rule cardinal_cong)
 apply (rule eqpoll_trans)
@@ -269,7 +269,7 @@
 
 lemma well_ord_cadd_cmult_distrib:
     "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |]
-     ==> (i |+| j) |*| k = (i |*| k) |+| (j |*| k)"
+     ==> (i \<oplus> j) \<otimes> k = (i \<otimes> k) \<oplus> (j \<otimes> k)"
 apply (unfold cadd_def cmult_def)
 apply (rule cardinal_cong)
 apply (rule eqpoll_trans)
@@ -290,7 +290,7 @@
 apply (rule lam_bijective, safe)
 done
 
-lemma cmult_0 [simp]: "0 |*| i = 0"
+lemma cmult_0 [simp]: "0 \<otimes> i = 0"
 by (simp add: cmult_def prod_0_eqpoll [THEN cardinal_cong])
 
 subsubsection{*1 is the identity for multiplication*}
@@ -301,7 +301,7 @@
 apply (rule singleton_prod_bij [THEN bij_converse_bij])
 done
 
-lemma cmult_1 [simp]: "Card(K) ==> 1 |*| K = K"
+lemma cmult_1 [simp]: "Card(K) ==> 1 \<otimes> K = K"
 apply (unfold cmult_def succ_def)
 apply (simp add: prod_singleton_eqpoll [THEN cardinal_cong] Card_cardinal_eq)
 done
@@ -314,7 +314,7 @@
 done
 
 (*Could probably weaken the premise to well_ord(K,r), or remove using AC*)
-lemma cmult_square_le: "Card(K) ==> K \<le> K |*| K"
+lemma cmult_square_le: "Card(K) ==> K \<le> K \<otimes> K"
 apply (unfold cmult_def)
 apply (rule le_trans)
 apply (rule_tac [2] well_ord_lepoll_imp_Card_le)
@@ -332,7 +332,7 @@
 
 (*Could probably weaken the premises to well_ord(K,r), or removing using AC*)
 lemma cmult_le_self:
-    "[| Card(K);  Ord(L);  0<L |] ==> K \<le> (K |*| L)"
+    "[| Card(K);  Ord(L);  0<L |] ==> K \<le> (K \<otimes> L)"
 apply (unfold cmult_def)
 apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le])
   apply assumption
@@ -353,7 +353,7 @@
 done
 
 lemma cmult_le_mono:
-    "[| K' \<le> K;  L' \<le> L |] ==> (K' |*| L') \<le> (K |*| L)"
+    "[| K' \<le> K;  L' \<le> L |] ==> (K' \<otimes> L') \<le> (K \<otimes> L)"
 apply (unfold cmult_def)
 apply (safe dest!: le_subset_iff [THEN iffD1])
 apply (rule well_ord_lepoll_imp_Card_le)
@@ -374,7 +374,7 @@
 
 (*Unconditional version requires AC*)
 lemma cmult_succ_lemma:
-    "[| Ord(m);  Ord(n) |] ==> succ(m) |*| n = n |+| (m |*| n)"
+    "[| Ord(m);  Ord(n) |] ==> succ(m) \<otimes> n = n \<oplus> (m \<otimes> n)"
 apply (unfold cmult_def cadd_def)
 apply (rule prod_succ_eqpoll [THEN cardinal_cong, THEN trans])
 apply (rule cardinal_cong [symmetric])
@@ -382,12 +382,12 @@
 apply (blast intro: well_ord_rmult well_ord_Memrel)
 done
 
-lemma nat_cmult_eq_mult: "[| m: nat;  n: nat |] ==> m |*| n = m#*n"
+lemma nat_cmult_eq_mult: "[| m: nat;  n: nat |] ==> m \<otimes> n = m#*n"
 apply (induct_tac m)
 apply (simp_all add: cmult_succ_lemma nat_cadd_eq_add)
 done
 
-lemma cmult_2: "Card(n) ==> 2 |*| n = n |+| n"
+lemma cmult_2: "Card(n) ==> 2 \<otimes> n = n \<oplus> n"
 by (simp add: cmult_succ_lemma Card_is_Ord cadd_commute [of _ 0])
 
 lemma sum_lepoll_prod: "2 \<lesssim> C ==> B+B \<lesssim> C*B"
@@ -555,7 +555,7 @@
 (*Kunen: "each <x,y>: K*K has no more than z*z predecessors..." (page 29) *)
 lemma ordermap_csquare_le:
   "[| Limit(K);  x<K;  y<K;  z=succ(x \<union> y) |]
-   ==> | ordermap(K*K, csquare_rel(K)) ` <x,y> | \<le> |succ(z)| |*| |succ(z)|"
+   ==> | ordermap(K*K, csquare_rel(K)) ` <x,y> | \<le> |succ(z)| \<otimes> |succ(z)|"
 apply (unfold cmult_def)
 apply (rule well_ord_rmult [THEN well_ord_lepoll_imp_Card_le])
 apply (rule Ord_cardinal [THEN well_ord_Memrel])+
@@ -575,7 +575,7 @@
 
 (*Kunen: "... so the order type is @{text"\<le>"} K" *)
 lemma ordertype_csquare_le:
-     "[| InfCard(K);  \<forall>y\<in>K. InfCard(y) \<longrightarrow> y |*| y = y |]
+     "[| InfCard(K);  \<forall>y\<in>K. InfCard(y) \<longrightarrow> y \<otimes> y = y |]
       ==> ordertype(K*K, csquare_rel(K)) \<le> K"
 apply (frule InfCard_is_Card [THEN Card_is_Ord])
 apply (rule all_lt_imp_le, assumption)
@@ -604,7 +604,7 @@
 done
 
 (*Main result: Kunen's Theorem 10.12*)
-lemma InfCard_csquare_eq: "InfCard(K) ==> K |*| K = K"
+lemma InfCard_csquare_eq: "InfCard(K) ==> K \<otimes> K = K"
 apply (frule InfCard_is_Card [THEN Card_is_Ord])
 apply (erule rev_mp)
 apply (erule_tac i=K in trans_induct)
@@ -639,7 +639,7 @@
 
 subsubsection{*Toward's Kunen's Corollary 10.13 (1)*}
 
-lemma InfCard_le_cmult_eq: "[| InfCard(K);  L \<le> K;  0<L |] ==> K |*| L = K"
+lemma InfCard_le_cmult_eq: "[| InfCard(K);  L \<le> K;  0<L |] ==> K \<otimes> L = K"
 apply (rule le_anti_sym)
  prefer 2
  apply (erule ltE, blast intro: cmult_le_self InfCard_is_Card)
@@ -649,7 +649,7 @@
 done
 
 (*Corollary 10.13 (1), for cardinal multiplication*)
-lemma InfCard_cmult_eq: "[| InfCard(K);  InfCard(L) |] ==> K |*| L = K \<union> L"
+lemma InfCard_cmult_eq: "[| InfCard(K);  InfCard(L) |] ==> K \<otimes> L = K \<union> L"
 apply (rule_tac i = K and j = L in Ord_linear_le)
 apply (typecheck add: InfCard_is_Card Card_is_Ord)
 apply (rule cmult_commute [THEN ssubst])
@@ -658,13 +658,13 @@
                      subset_Un_iff2 [THEN iffD1] le_imp_subset)
 done
 
-lemma InfCard_cdouble_eq: "InfCard(K) ==> K |+| K = K"
+lemma InfCard_cdouble_eq: "InfCard(K) ==> K \<oplus> K = K"
 apply (simp add: cmult_2 [symmetric] InfCard_is_Card cmult_commute)
 apply (simp add: InfCard_le_cmult_eq InfCard_is_Limit Limit_has_0 Limit_has_succ)
 done
 
 (*Corollary 10.13 (1), for cardinal addition*)
-lemma InfCard_le_cadd_eq: "[| InfCard(K);  L \<le> K |] ==> K |+| L = K"
+lemma InfCard_le_cadd_eq: "[| InfCard(K);  L \<le> K |] ==> K \<oplus> L = K"
 apply (rule le_anti_sym)
  prefer 2
  apply (erule ltE, blast intro: cadd_le_self InfCard_is_Card)
@@ -673,7 +673,7 @@
 apply (simp add: InfCard_cdouble_eq)
 done
 
-lemma InfCard_cadd_eq: "[| InfCard(K);  InfCard(L) |] ==> K |+| L = K \<union> L"
+lemma InfCard_cadd_eq: "[| InfCard(K);  InfCard(L) |] ==> K \<oplus> L = K \<union> L"
 apply (rule_tac i = K and j = L in Ord_linear_le)
 apply (typecheck add: InfCard_is_Card Card_is_Ord)
 apply (rule cadd_commute [THEN ssubst])
@@ -704,7 +704,7 @@
 
 (*Allows selective unfolding.  Less work than deriving intro/elim rules*)
 lemma jump_cardinal_iff:
-     "i \<in> jump_cardinal(K) <->
+     "i \<in> jump_cardinal(K) \<longleftrightarrow>
       (\<exists>r X. r \<subseteq> K*K & X \<subseteq> K & well_ord(X,r) & i = ordertype(X,r))"
 apply (unfold jump_cardinal_def)
 apply (blast del: subsetI)
@@ -766,7 +766,7 @@
 apply (blast intro: Card_is_Ord)+
 done
 
-lemma lt_csucc_iff: "[| Ord(i); Card(K) |] ==> i < csucc(K) <-> |i| \<le> K"
+lemma lt_csucc_iff: "[| Ord(i); Card(K) |] ==> i < csucc(K) \<longleftrightarrow> |i| \<le> K"
 apply (rule iffI)
 apply (rule_tac [2] Card_lt_imp_lt)
 apply (erule_tac [2] lt_trans1)
@@ -778,7 +778,7 @@
 done
 
 lemma Card_lt_csucc_iff:
-     "[| Card(K'); Card(K) |] ==> K' < csucc(K) <-> K' \<le> K"
+     "[| Card(K'); Card(K) |] ==> K' < csucc(K) \<longleftrightarrow> K' \<le> K"
 by (simp add: lt_csucc_iff Card_cardinal_eq Card_is_Ord)
 
 lemma InfCard_csucc: "InfCard(K) ==> InfCard(csucc(K))"
diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/Cardinal_AC.thy
--- a/src/ZF/Cardinal_AC.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Cardinal_AC.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -25,7 +25,7 @@
 apply (rule well_ord_cardinal_eqE, assumption+)
 done
 
-lemma cardinal_eqpoll_iff: "|X| = |Y| <-> X eqpoll Y"
+lemma cardinal_eqpoll_iff: "|X| = |Y| \<longleftrightarrow> X eqpoll Y"
 by (blast intro: cardinal_cong cardinal_eqE)
 
 lemma cardinal_disjoint_Un:
@@ -38,21 +38,21 @@
 apply (erule well_ord_lepoll_imp_Card_le, assumption)
 done
 
-lemma cadd_assoc: "(i |+| j) |+| k = i |+| (j |+| k)"
+lemma cadd_assoc: "(i \<oplus> j) \<oplus> k = i \<oplus> (j \<oplus> k)"
 apply (rule AC_well_ord [THEN exE])
 apply (rule AC_well_ord [THEN exE])
 apply (rule AC_well_ord [THEN exE])
 apply (rule well_ord_cadd_assoc, assumption+)
 done
 
-lemma cmult_assoc: "(i |*| j) |*| k = i |*| (j |*| k)"
+lemma cmult_assoc: "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
 apply (rule AC_well_ord [THEN exE])
 apply (rule AC_well_ord [THEN exE])
 apply (rule AC_well_ord [THEN exE])
 apply (rule well_ord_cmult_assoc, assumption+)
 done
 
-lemma cadd_cmult_distrib: "(i |+| j) |*| k = (i |*| k) |+| (j |*| k)"
+lemma cadd_cmult_distrib: "(i \<oplus> j) \<otimes> k = (i \<otimes> k) \<oplus> (j \<otimes> k)"
 apply (rule AC_well_ord [THEN exE])
 apply (rule AC_well_ord [THEN exE])
 apply (rule AC_well_ord [THEN exE])
@@ -74,19 +74,19 @@
 apply (rule cardinal_eqpoll [THEN eqpoll_imp_lepoll])
 done
 
-lemma le_Card_iff: "Card(K) ==> |A| \<le> K <-> A lepoll K"
+lemma le_Card_iff: "Card(K) ==> |A| \<le> K \<longleftrightarrow> A lepoll K"
 apply (erule Card_cardinal_eq [THEN subst], rule iffI,
        erule Card_le_imp_lepoll)
 apply (erule lepoll_imp_Card_le)
 done
 
-lemma cardinal_0_iff_0 [simp]: "|A| = 0 <-> A = 0";
+lemma cardinal_0_iff_0 [simp]: "|A| = 0 \<longleftrightarrow> A = 0";
 apply auto
 apply (drule cardinal_0 [THEN ssubst])
 apply (blast intro: eqpoll_0_iff [THEN iffD1] cardinal_eqpoll_iff [THEN iffD1])
 done
 
-lemma cardinal_lt_iff_lesspoll: "Ord(i) ==> i < |A| <-> i lesspoll A"
+lemma cardinal_lt_iff_lesspoll: "Ord(i) ==> i < |A| \<longleftrightarrow> i lesspoll A"
 apply (cut_tac A = "A" in cardinal_eqpoll)
 apply (auto simp add: eqpoll_iff)
 apply (blast intro: lesspoll_trans2 lt_Card_imp_lesspoll Card_cardinal)
diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/EquivClass.thy
--- a/src/ZF/EquivClass.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/EquivClass.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -92,11 +92,11 @@
 by (unfold equiv_def, blast)
 
 lemma equiv_class_eq_iff:
-     "equiv(A,r) ==> <x,y>: r <-> r``{x} = r``{y} & x:A & y:A"
+     "equiv(A,r) ==> <x,y>: r \<longleftrightarrow> r``{x} = r``{y} & x:A & y:A"
 by (blast intro: eq_equiv_class equiv_class_eq dest: equiv_type)
 
 lemma eq_equiv_class_iff:
-     "[| equiv(A,r);  x: A;  y: A |] ==> r``{x} = r``{y} <-> <x,y>: r"
+     "[| equiv(A,r);  x: A;  y: A |] ==> r``{x} = r``{y} \<longleftrightarrow> <x,y>: r"
 by (blast intro: eq_equiv_class equiv_class_eq dest: equiv_type)
 
 (*** Quotients ***)
diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/Finite.thy
--- a/src/ZF/Finite.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Finite.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -183,7 +183,7 @@
 
 lemma FiniteFun_Collect_iff:
      "f \<in> FiniteFun(A, {y:B. P(y)})
-      <-> f \<in> FiniteFun(A,B) & (\<forall>x\<in>domain(f). P(f`x))"
+      \<longleftrightarrow> f \<in> FiniteFun(A,B) & (\<forall>x\<in>domain(f). P(f`x))"
 apply auto
 apply (blast intro: FiniteFun_mono [THEN [2] rev_subsetD])
 apply (blast dest: Pair_mem_PiD FiniteFun_is_fun)
diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/Inductive_ZF.thy
--- a/src/ZF/Inductive_ZF.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Inductive_ZF.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -22,7 +22,7 @@
   ("Tools/primrec_package.ML")
 begin
 
-lemma def_swap_iff: "a == b ==> a = c <-> c = b"
+lemma def_swap_iff: "a == b ==> a = c \<longleftrightarrow> c = b"
   by blast
 
 lemma def_trans: "f == g ==> g(a) = b ==> f(a) = b"
diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/IntArith.thy
--- a/src/ZF/IntArith.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/IntArith.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -31,13 +31,13 @@
 
 (** Combining of literal coefficients in sums of products **)
 
-lemma zless_iff_zdiff_zless_0: "(x $< y) <-> (x$-y $< #0)"
+lemma zless_iff_zdiff_zless_0: "(x $< y) \<longleftrightarrow> (x$-y $< #0)"
   by (simp add: zcompare_rls)
 
-lemma eq_iff_zdiff_eq_0: "[| x: int; y: int |] ==> (x = y) <-> (x$-y = #0)"
+lemma eq_iff_zdiff_eq_0: "[| x: int; y: int |] ==> (x = y) \<longleftrightarrow> (x$-y = #0)"
   by (simp add: zcompare_rls)
 
-lemma zle_iff_zdiff_zle_0: "(x $<= y) <-> (x$-y $<= #0)"
+lemma zle_iff_zdiff_zle_0: "(x $<= y) \<longleftrightarrow> (x$-y $<= #0)"
   by (simp add: zcompare_rls)
 
 
@@ -58,33 +58,33 @@
   zle_iff_zdiff_zle_0 [where y = n]
   for u v (* FIXME n (!?) *)
 
-lemma eq_add_iff1: "(i$*u $+ m = j$*u $+ n) <-> ((i$-j)$*u $+ m = intify(n))"
+lemma eq_add_iff1: "(i$*u $+ m = j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m = intify(n))"
   apply (simp add: zdiff_def zadd_zmult_distrib)
   apply (simp add: zcompare_rls)
   apply (simp add: zadd_ac)
   done
 
-lemma eq_add_iff2: "(i$*u $+ m = j$*u $+ n) <-> (intify(m) = (j$-i)$*u $+ n)"
+lemma eq_add_iff2: "(i$*u $+ m = j$*u $+ n) \<longleftrightarrow> (intify(m) = (j$-i)$*u $+ n)"
   apply (simp add: zdiff_def zadd_zmult_distrib)
   apply (simp add: zcompare_rls)
   apply (simp add: zadd_ac)
   done
 
-lemma less_add_iff1: "(i$*u $+ m $< j$*u $+ n) <-> ((i$-j)$*u $+ m $< n)"
+lemma less_add_iff1: "(i$*u $+ m $< j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m $< n)"
   apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)
   done
 
-lemma less_add_iff2: "(i$*u $+ m $< j$*u $+ n) <-> (m $< (j$-i)$*u $+ n)"
+lemma less_add_iff2: "(i$*u $+ m $< j$*u $+ n) \<longleftrightarrow> (m $< (j$-i)$*u $+ n)"
   apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)
   done
 
-lemma le_add_iff1: "(i$*u $+ m $<= j$*u $+ n) <-> ((i$-j)$*u $+ m $<= n)"
+lemma le_add_iff1: "(i$*u $+ m $<= j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m $<= n)"
   apply (simp add: zdiff_def zadd_zmult_distrib)
   apply (simp add: zcompare_rls)
   apply (simp add: zadd_ac)
   done
 
-lemma le_add_iff2: "(i$*u $+ m $<= j$*u $+ n) <-> (m $<= (j$-i)$*u $+ n)"
+lemma le_add_iff2: "(i$*u $+ m $<= j$*u $+ n) \<longleftrightarrow> (m $<= (j$-i)$*u $+ n)"
   apply (simp add: zdiff_def zadd_zmult_distrib)
   apply (simp add: zcompare_rls)
   apply (simp add: zadd_ac)
diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/IntDiv_ZF.thy
--- a/src/ZF/IntDiv_ZF.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/IntDiv_ZF.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -136,7 +136,7 @@
 (*** Inequality lemmas involving $#succ(m) ***)
 
 lemma zless_add_succ_iff:
-     "(w $< z $+ $# succ(m)) <-> (w $< z $+ $#m | intify(w) = z $+ $#m)"
+     "(w $< z $+ $# succ(m)) \<longleftrightarrow> (w $< z $+ $#m | intify(w) = z $+ $#m)"
 apply (auto simp add: zless_iff_succ_zadd zadd_assoc int_of_add [symmetric])
 apply (rule_tac [3] x = "0" in bexI)
 apply (cut_tac m = "m" in int_succ_int_1)
@@ -149,32 +149,32 @@
 done
 
 lemma zadd_succ_lemma:
-     "z \<in> int ==> (w $+ $# succ(m) $<= z) <-> (w $+ $#m $< z)"
+     "z \<in> int ==> (w $+ $# succ(m) $<= z) \<longleftrightarrow> (w $+ $#m $< z)"
 apply (simp only: not_zless_iff_zle [THEN iff_sym] zless_add_succ_iff)
 apply (auto intro: zle_anti_sym elim: zless_asym
             simp add: zless_imp_zle not_zless_iff_zle)
 done
 
-lemma zadd_succ_zle_iff: "(w $+ $# succ(m) $<= z) <-> (w $+ $#m $< z)"
+lemma zadd_succ_zle_iff: "(w $+ $# succ(m) $<= z) \<longleftrightarrow> (w $+ $#m $< z)"
 apply (cut_tac z = "intify (z)" in zadd_succ_lemma)
 apply auto
 done
 
 (** Inequality reasoning **)
 
-lemma zless_add1_iff_zle: "(w $< z $+ #1) <-> (w$<=z)"
+lemma zless_add1_iff_zle: "(w $< z $+ #1) \<longleftrightarrow> (w$<=z)"
 apply (subgoal_tac "#1 = $# 1")
 apply (simp only: zless_add_succ_iff zle_def)
 apply auto
 done
 
-lemma add1_zle_iff: "(w $+ #1 $<= z) <-> (w $< z)"
+lemma add1_zle_iff: "(w $+ #1 $<= z) \<longleftrightarrow> (w $< z)"
 apply (subgoal_tac "#1 = $# 1")
 apply (simp only: zadd_succ_zle_iff)
 apply auto
 done
 
-lemma add1_left_zle_iff: "(#1 $+ w $<= z) <-> (w $< z)"
+lemma add1_left_zle_iff: "(#1 $+ w $<= z) \<longleftrightarrow> (w $< z)"
 apply (subst zadd_commute)
 apply (rule add1_zle_iff)
 done
@@ -280,13 +280,13 @@
 (** Products of zeroes **)
 
 lemma zmult_eq_lemma:
-     "[| m \<in> int; n \<in> int |] ==> (m = #0 | n = #0) <-> (m$*n = #0)"
+     "[| m \<in> int; n \<in> int |] ==> (m = #0 | n = #0) \<longleftrightarrow> (m$*n = #0)"
 apply (case_tac "m $< #0")
 apply (auto simp add: not_zless_iff_zle zle_def neq_iff_zless)
 apply (force dest: zmult_zless_mono1_neg zmult_zless_mono1)+
 done
 
-lemma zmult_eq_0_iff [iff]: "(m$*n = #0) <-> (intify(m) = #0 | intify(n) = #0)"
+lemma zmult_eq_0_iff [iff]: "(m$*n = #0) \<longleftrightarrow> (intify(m) = #0 | intify(n) = #0)"
 apply (simp add: zmult_eq_lemma)
 done
 
@@ -296,7 +296,7 @@
 
 lemma zmult_zless_lemma:
      "[| k \<in> int; m \<in> int; n \<in> int |]
-      ==> (m$*k $< n$*k) <-> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
+      ==> (m$*k $< n$*k) \<longleftrightarrow> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
 apply (case_tac "k = #0")
 apply (auto simp add: neq_iff_zless zmult_zless_mono1 zmult_zless_mono1_neg)
 apply (auto simp add: not_zless_iff_zle
@@ -307,43 +307,43 @@
 done
 
 lemma zmult_zless_cancel2:
-     "(m$*k $< n$*k) <-> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
+     "(m$*k $< n$*k) \<longleftrightarrow> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
 apply (cut_tac k = "intify (k)" and m = "intify (m)" and n = "intify (n)"
        in zmult_zless_lemma)
 apply auto
 done
 
 lemma zmult_zless_cancel1:
-     "(k$*m $< k$*n) <-> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
+     "(k$*m $< k$*n) \<longleftrightarrow> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
 by (simp add: zmult_commute [of k] zmult_zless_cancel2)
 
 lemma zmult_zle_cancel2:
-     "(m$*k $<= n$*k) <-> ((#0 $< k \<longrightarrow> m$<=n) & (k $< #0 \<longrightarrow> n$<=m))"
+     "(m$*k $<= n$*k) \<longleftrightarrow> ((#0 $< k \<longrightarrow> m$<=n) & (k $< #0 \<longrightarrow> n$<=m))"
 by (auto simp add: not_zless_iff_zle [THEN iff_sym] zmult_zless_cancel2)
 
 lemma zmult_zle_cancel1:
-     "(k$*m $<= k$*n) <-> ((#0 $< k \<longrightarrow> m$<=n) & (k $< #0 \<longrightarrow> n$<=m))"
+     "(k$*m $<= k$*n) \<longleftrightarrow> ((#0 $< k \<longrightarrow> m$<=n) & (k $< #0 \<longrightarrow> n$<=m))"
 by (auto simp add: not_zless_iff_zle [THEN iff_sym] zmult_zless_cancel1)
 
-lemma int_eq_iff_zle: "[| m \<in> int; n \<in> int |] ==> m=n <-> (m $<= n & n $<= m)"
+lemma int_eq_iff_zle: "[| m \<in> int; n \<in> int |] ==> m=n \<longleftrightarrow> (m $<= n & n $<= m)"
 apply (blast intro: zle_refl zle_anti_sym)
 done
 
 lemma zmult_cancel2_lemma:
-     "[| k \<in> int; m \<in> int; n \<in> int |] ==> (m$*k = n$*k) <-> (k=#0 | m=n)"
+     "[| k \<in> int; m \<in> int; n \<in> int |] ==> (m$*k = n$*k) \<longleftrightarrow> (k=#0 | m=n)"
 apply (simp add: int_eq_iff_zle [of "m$*k"] int_eq_iff_zle [of m])
 apply (auto simp add: zmult_zle_cancel2 neq_iff_zless)
 done
 
 lemma zmult_cancel2 [simp]:
-     "(m$*k = n$*k) <-> (intify(k) = #0 | intify(m) = intify(n))"
+     "(m$*k = n$*k) \<longleftrightarrow> (intify(k) = #0 | intify(m) = intify(n))"
 apply (rule iff_trans)
 apply (rule_tac [2] zmult_cancel2_lemma)
 apply auto
 done
 
 lemma zmult_cancel1 [simp]:
-     "(k$*m = k$*n) <-> (intify(k) = #0 | intify(m) = intify(n))"
+     "(k$*m = k$*n) \<longleftrightarrow> (intify(k) = #0 | intify(m) = intify(n))"
 by (simp add: zmult_commute [of k] zmult_cancel2)
 
 
@@ -458,7 +458,7 @@
 
 (*FIXME: use intify in integ_of so that we always have @{term"integ_of w \<in> int"}.
     then this rewrite can work for all constants!!*)
-lemma intify_eq_0_iff_zle: "intify(m) = #0 <-> (m $<= #0 & #0 $<= m)"
+lemma intify_eq_0_iff_zle: "intify(m) = #0 \<longleftrightarrow> (m $<= #0 & #0 $<= m)"
 apply (simp (no_asm) add: int_eq_iff_zle)
 done
 
@@ -484,7 +484,7 @@
 
 lemma int_0_less_lemma:
      "[| x \<in> int; y \<in> int |]
-      ==> (#0 $< x $* y) <-> (#0 $< x & #0 $< y | x $< #0 & y $< #0)"
+      ==> (#0 $< x $* y) \<longleftrightarrow> (#0 $< x & #0 $< y | x $< #0 & y $< #0)"
 apply (auto simp add: zle_def not_zless_iff_zle zmult_pos zmult_neg)
 apply (rule ccontr)
 apply (rule_tac [2] ccontr)
@@ -498,30 +498,30 @@
 done
 
 lemma int_0_less_mult_iff:
-     "(#0 $< x $* y) <-> (#0 $< x & #0 $< y | x $< #0 & y $< #0)"
+     "(#0 $< x $* y) \<longleftrightarrow> (#0 $< x & #0 $< y | x $< #0 & y $< #0)"
 apply (cut_tac x = "intify (x)" and y = "intify (y)" in int_0_less_lemma)
 apply auto
 done
 
 lemma int_0_le_lemma:
      "[| x \<in> int; y \<in> int |]
-      ==> (#0 $<= x $* y) <-> (#0 $<= x & #0 $<= y | x $<= #0 & y $<= #0)"
+      ==> (#0 $<= x $* y) \<longleftrightarrow> (#0 $<= x & #0 $<= y | x $<= #0 & y $<= #0)"
 by (auto simp add: zle_def not_zless_iff_zle int_0_less_mult_iff)
 
 lemma int_0_le_mult_iff:
-     "(#0 $<= x $* y) <-> ((#0 $<= x & #0 $<= y) | (x $<= #0 & y $<= #0))"
+     "(#0 $<= x $* y) \<longleftrightarrow> ((#0 $<= x & #0 $<= y) | (x $<= #0 & y $<= #0))"
 apply (cut_tac x = "intify (x)" and y = "intify (y)" in int_0_le_lemma)
 apply auto
 done
 
 lemma zmult_less_0_iff:
-     "(x $* y $< #0) <-> (#0 $< x & y $< #0 | x $< #0 & #0 $< y)"
+     "(x $* y $< #0) \<longleftrightarrow> (#0 $< x & y $< #0 | x $< #0 & #0 $< y)"
 apply (auto simp add: int_0_le_mult_iff not_zle_iff_zless [THEN iff_sym])
 apply (auto dest: zless_not_sym simp add: not_zle_iff_zless)
 done
 
 lemma zmult_le_0_iff:
-     "(x $* y $<= #0) <-> (#0 $<= x & y $<= #0 | x $<= #0 & #0 $<= y)"
+     "(x $* y $<= #0) \<longleftrightarrow> (#0 $<= x & y $<= #0 | x $<= #0 & #0 $<= y)"
 by (auto dest: zless_not_sym
          simp add: int_0_less_mult_iff not_zless_iff_zle [THEN iff_sym])
 
@@ -1656,7 +1656,7 @@
 apply auto
 done
 
-lemma pos_imp_zdiv_nonneg_iff: "#0 $< b ==> (#0 $<= a zdiv b) <-> (#0 $<= a)"
+lemma pos_imp_zdiv_nonneg_iff: "#0 $< b ==> (#0 $<= a zdiv b) \<longleftrightarrow> (#0 $<= a)"
 apply auto
 apply (drule_tac [2] zdiv_mono1)
 apply (auto simp add: neq_iff_zless)
@@ -1664,7 +1664,7 @@
 apply (blast intro: zdiv_neg_pos_less0)
 done
 
-lemma neg_imp_zdiv_nonneg_iff: "b $< #0 ==> (#0 $<= a zdiv b) <-> (a $<= #0)"
+lemma neg_imp_zdiv_nonneg_iff: "b $< #0 ==> (#0 $<= a zdiv b) \<longleftrightarrow> (a $<= #0)"
 apply (subst zdiv_zminus_zminus [symmetric])
 apply (rule iff_trans)
 apply (rule pos_imp_zdiv_nonneg_iff)
@@ -1672,13 +1672,13 @@
 done
 
 (*But not (a zdiv b $<= 0 iff a$<=0); consider a=1, b=2 when a zdiv b = 0.*)
-lemma pos_imp_zdiv_neg_iff: "#0 $< b ==> (a zdiv b $< #0) <-> (a $< #0)"
+lemma pos_imp_zdiv_neg_iff: "#0 $< b ==> (a zdiv b $< #0) \<longleftrightarrow> (a $< #0)"
 apply (simp (no_asm_simp) add: not_zle_iff_zless [THEN iff_sym])
 apply (erule pos_imp_zdiv_nonneg_iff)
 done
 
 (*Again the law fails for $<=: consider a = -1, b = -2 when a zdiv b = 0*)
-lemma neg_imp_zdiv_neg_iff: "b $< #0 ==> (a zdiv b $< #0) <-> (#0 $< a)"
+lemma neg_imp_zdiv_neg_iff: "b $< #0 ==> (a zdiv b $< #0) \<longleftrightarrow> (#0 $< a)"
 apply (simp (no_asm_simp) add: not_zle_iff_zless [THEN iff_sym])
 apply (erule neg_imp_zdiv_nonneg_iff)
 done
@@ -1710,8 +1710,8 @@
  done
 
 
- lemma neg_zdiv_mult_2: "a $<= #0 ==> (#1 $+ #2$*b) zdiv (#2$*a) <-> (b$+#1) zdiv a"
- apply (subgoal_tac " (#1 $+ #2$* ($-b-#1)) zdiv (#2 $* ($-a)) <-> ($-b-#1) zdiv ($-a)")
+ lemma neg_zdiv_mult_2: "a $<= #0 ==> (#1 $+ #2$*b) zdiv (#2$*a) \<longleftrightarrow> (b$+#1) zdiv a"
+ apply (subgoal_tac " (#1 $+ #2$* ($-b-#1)) zdiv (#2 $* ($-a)) \<longleftrightarrow> ($-b-#1) zdiv ($-a)")
  apply (rule_tac [2] pos_zdiv_mult_2)
  apply (auto simp add: zmult_zminus_right)
  apply (subgoal_tac " (#-1 - (#2 $* b)) = - (#1 $+ (#2 $* b))")
diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/Int_ZF.thy
--- a/src/ZF/Int_ZF.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Int_ZF.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -107,7 +107,7 @@
 (** Natural deduction for intrel **)
 
 lemma intrel_iff [simp]: 
-    "<<x1,y1>,<x2,y2>>: intrel <->  
+    "<<x1,y1>,<x2,y2>>: intrel \<longleftrightarrow>  
      x1\<in>nat & y1\<in>nat & x2\<in>nat & y2\<in>nat & x1#+y2 = x2#+y1"
 by (simp add: intrel_def)
 
@@ -148,7 +148,7 @@
 lemma int_of_type [simp,TC]: "$#m \<in> int"
 by (simp add: int_def quotient_def int_of_def, auto)
 
-lemma int_of_eq [iff]: "($# m = $# n) <-> natify(m)=natify(n)"
+lemma int_of_eq [iff]: "($# m = $# n) \<longleftrightarrow> natify(m)=natify(n)"
 by (simp add: int_of_def)
 
 lemma int_of_inject: "[| $#m = $#n;  m\<in>nat;  n\<in>nat |] ==> m=n"
@@ -202,16 +202,16 @@
 
 (** Orderings **)
 
-lemma zless_intify1 [simp]:"intify(x) $< y <-> x $< y"
+lemma zless_intify1 [simp]:"intify(x) $< y \<longleftrightarrow> x $< y"
 by (simp add: zless_def)
 
-lemma zless_intify2 [simp]:"x $< intify(y) <-> x $< y"
+lemma zless_intify2 [simp]:"x $< intify(y) \<longleftrightarrow> x $< y"
 by (simp add: zless_def)
 
-lemma zle_intify1 [simp]:"intify(x) $<= y <-> x $<= y"
+lemma zle_intify1 [simp]:"intify(x) $<= y \<longleftrightarrow> x $<= y"
 by (simp add: zle_def)
 
-lemma zle_intify2 [simp]:"x $<= intify(y) <-> x $<= y"
+lemma zle_intify2 [simp]:"x $<= intify(y) \<longleftrightarrow> x $<= y"
 by (simp add: zle_def)
 
 
@@ -268,7 +268,7 @@
 
 subsection{*@{term znegative}: the test for negative integers*}
 
-lemma znegative: "[| x\<in>nat; y\<in>nat |] ==> znegative(intrel``{<x,y>}) <-> x<y"
+lemma znegative: "[| x\<in>nat; y\<in>nat |] ==> znegative(intrel``{<x,y>}) \<longleftrightarrow> x<y"
 apply (cases "x<y") 
 apply (auto simp add: znegative_def not_lt_iff_le)
 apply (subgoal_tac "y #+ x2 < x #+ y2", force) 
@@ -644,7 +644,7 @@
 lemma zless_not_refl [iff]: "~ (z$<z)"
 by (auto simp add: zless_def znegative_def int_of_def zdiff_def)
 
-lemma neq_iff_zless: "[| x: int; y: int |] ==> (x \<noteq> y) <-> (x $< y | y $< x)"
+lemma neq_iff_zless: "[| x: int; y: int |] ==> (x \<noteq> y) \<longleftrightarrow> (x $< y | y $< x)"
 by (cut_tac z = x and w = y in zless_linear, auto)
 
 lemma zless_imp_intify_neq: "w $< z ==> intify(w) \<noteq> intify(z)"
@@ -682,14 +682,14 @@
 by (cut_tac intify_in_int [THEN zless_succ_zadd_lemma], auto)
 
 lemma zless_iff_succ_zadd:
-     "w $< z <-> (\<exists>n\<in>nat. w $+ $#(succ(n)) = intify(z))"
+     "w $< z \<longleftrightarrow> (\<exists>n\<in>nat. w $+ $#(succ(n)) = intify(z))"
 apply (rule iffI)
 apply (erule zless_imp_succ_zadd, auto)
 apply (rename_tac "n")
 apply (cut_tac w = w and n = n in zless_succ_zadd, auto)
 done
 
-lemma zless_int_of [simp]: "[| m\<in>nat; n\<in>nat |] ==> ($#m $< $#n) <-> (m<n)"
+lemma zless_int_of [simp]: "[| m\<in>nat; n\<in>nat |] ==> ($#m $< $#n) \<longleftrightarrow> (m<n)"
 apply (simp add: less_iff_succ_add zless_iff_succ_zadd int_of_add [symmetric])
 apply (blast intro: sym)
 done
@@ -768,13 +768,13 @@
 apply (simp add: zless_def zdiff_def zminus_def)
 done
 
-lemma not_zless_iff_zle: "~ (z $< w) <-> (w $<= z)"
+lemma not_zless_iff_zle: "~ (z $< w) \<longleftrightarrow> (w $<= z)"
 apply (cut_tac z = z and w = w in zless_linear)
 apply (auto dest: zless_trans simp add: zle_def)
 apply (auto dest!: zless_imp_intify_neq)
 done
 
-lemma not_zle_iff_zless: "~ (z $<= w) <-> (w $< z)"
+lemma not_zle_iff_zless: "~ (z $<= w) \<longleftrightarrow> (w $< z)"
 by (simp add: not_zless_iff_zle [THEN iff_sym])
 
 
@@ -786,32 +786,32 @@
 lemma zdiff_zdiff_eq2: "x $- (y $- z) = (x $+ z) $- y"
 by (simp add: zdiff_def zadd_ac)
 
-lemma zdiff_zless_iff: "(x$-y $< z) <-> (x $< z $+ y)"
+lemma zdiff_zless_iff: "(x$-y $< z) \<longleftrightarrow> (x $< z $+ y)"
 by (simp add: zless_def zdiff_def zadd_ac)
 
-lemma zless_zdiff_iff: "(x $< z$-y) <-> (x $+ y $< z)"
+lemma zless_zdiff_iff: "(x $< z$-y) \<longleftrightarrow> (x $+ y $< z)"
 by (simp add: zless_def zdiff_def zadd_ac)
 
-lemma zdiff_eq_iff: "[| x: int; z: int |] ==> (x$-y = z) <-> (x = z $+ y)"
+lemma zdiff_eq_iff: "[| x: int; z: int |] ==> (x$-y = z) \<longleftrightarrow> (x = z $+ y)"
 by (auto simp add: zdiff_def zadd_assoc)
 
-lemma eq_zdiff_iff: "[| x: int; z: int |] ==> (x = z$-y) <-> (x $+ y = z)"
+lemma eq_zdiff_iff: "[| x: int; z: int |] ==> (x = z$-y) \<longleftrightarrow> (x $+ y = z)"
 by (auto simp add: zdiff_def zadd_assoc)
 
 lemma zdiff_zle_iff_lemma:
-     "[| x: int; z: int |] ==> (x$-y $<= z) <-> (x $<= z $+ y)"
+     "[| x: int; z: int |] ==> (x$-y $<= z) \<longleftrightarrow> (x $<= z $+ y)"
 by (auto simp add: zle_def zdiff_eq_iff zdiff_zless_iff)
 
-lemma zdiff_zle_iff: "(x$-y $<= z) <-> (x $<= z $+ y)"
+lemma zdiff_zle_iff: "(x$-y $<= z) \<longleftrightarrow> (x $<= z $+ y)"
 by (cut_tac zdiff_zle_iff_lemma [OF intify_in_int intify_in_int], simp)
 
 lemma zle_zdiff_iff_lemma:
-     "[| x: int; z: int |] ==>(x $<= z$-y) <-> (x $+ y $<= z)"
+     "[| x: int; z: int |] ==>(x $<= z$-y) \<longleftrightarrow> (x $+ y $<= z)"
 apply (auto simp add: zle_def zdiff_eq_iff zless_zdiff_iff)
 apply (auto simp add: zdiff_def zadd_assoc)
 done
 
-lemma zle_zdiff_iff: "(x $<= z$-y) <-> (x $+ y $<= z)"
+lemma zle_zdiff_iff: "(x $<= z$-y) \<longleftrightarrow> (x $+ y $<= z)"
 by (cut_tac zle_zdiff_iff_lemma [ OF intify_in_int intify_in_int], simp)
 
 text{*This list of rewrites simplifies (in)equalities by bringing subtractions
@@ -828,41 +828,41 @@
      of the CancelNumerals Simprocs*}
 
 lemma zadd_left_cancel:
-     "[| w: int; w': int |] ==> (z $+ w' = z $+ w) <-> (w' = w)"
+     "[| w: int; w': int |] ==> (z $+ w' = z $+ w) \<longleftrightarrow> (w' = w)"
 apply safe
 apply (drule_tac t = "%x. x $+ ($-z) " in subst_context)
 apply (simp add: zadd_ac)
 done
 
 lemma zadd_left_cancel_intify [simp]:
-     "(z $+ w' = z $+ w) <-> intify(w') = intify(w)"
+     "(z $+ w' = z $+ w) \<longleftrightarrow> intify(w') = intify(w)"
 apply (rule iff_trans)
 apply (rule_tac [2] zadd_left_cancel, auto)
 done
 
 lemma zadd_right_cancel:
-     "[| w: int; w': int |] ==> (w' $+ z = w $+ z) <-> (w' = w)"
+     "[| w: int; w': int |] ==> (w' $+ z = w $+ z) \<longleftrightarrow> (w' = w)"
 apply safe
 apply (drule_tac t = "%x. x $+ ($-z) " in subst_context)
 apply (simp add: zadd_ac)
 done
 
 lemma zadd_right_cancel_intify [simp]:
-     "(w' $+ z = w $+ z) <-> intify(w') = intify(w)"
+     "(w' $+ z = w $+ z) \<longleftrightarrow> intify(w') = intify(w)"
 apply (rule iff_trans)
 apply (rule_tac [2] zadd_right_cancel, auto)
 done
 
-lemma zadd_right_cancel_zless [simp]: "(w' $+ z $< w $+ z) <-> (w' $< w)"
+lemma zadd_right_cancel_zless [simp]: "(w' $+ z $< w $+ z) \<longleftrightarrow> (w' $< w)"
 by (simp add: zdiff_zless_iff [THEN iff_sym] zdiff_def zadd_assoc)
 
-lemma zadd_left_cancel_zless [simp]: "(z $+ w' $< z $+ w) <-> (w' $< w)"
+lemma zadd_left_cancel_zless [simp]: "(z $+ w' $< z $+ w) \<longleftrightarrow> (w' $< w)"
 by (simp add: zadd_commute [of z] zadd_right_cancel_zless)
 
-lemma zadd_right_cancel_zle [simp]: "(w' $+ z $<= w $+ z) <-> w' $<= w"
+lemma zadd_right_cancel_zle [simp]: "(w' $+ z $<= w $+ z) \<longleftrightarrow> w' $<= w"
 by (simp add: zle_def)
 
-lemma zadd_left_cancel_zle [simp]: "(z $+ w' $<= z $+ w) <->  w' $<= w"
+lemma zadd_left_cancel_zle [simp]: "(z $+ w' $<= z $+ w) \<longleftrightarrow>  w' $<= w"
 by (simp add: zadd_commute [of z]  zadd_right_cancel_zle)
 
 
@@ -887,26 +887,26 @@
 
 subsection{*Comparison laws*}
 
-lemma zminus_zless_zminus [simp]: "($- x $< $- y) <-> (y $< x)"
+lemma zminus_zless_zminus [simp]: "($- x $< $- y) \<longleftrightarrow> (y $< x)"
 by (simp add: zless_def zdiff_def zadd_ac)
 
-lemma zminus_zle_zminus [simp]: "($- x $<= $- y) <-> (y $<= x)"
+lemma zminus_zle_zminus [simp]: "($- x $<= $- y) \<longleftrightarrow> (y $<= x)"
 by (simp add: not_zless_iff_zle [THEN iff_sym])
 
 subsubsection{*More inequality lemmas*}
 
-lemma equation_zminus: "[| x: int;  y: int |] ==> (x = $- y) <-> (y = $- x)"
+lemma equation_zminus: "[| x: int;  y: int |] ==> (x = $- y) \<longleftrightarrow> (y = $- x)"
 by auto
 
-lemma zminus_equation: "[| x: int;  y: int |] ==> ($- x = y) <-> ($- y = x)"
+lemma zminus_equation: "[| x: int;  y: int |] ==> ($- x = y) \<longleftrightarrow> ($- y = x)"
 by auto
 
-lemma equation_zminus_intify: "(intify(x) = $- y) <-> (intify(y) = $- x)"
+lemma equation_zminus_intify: "(intify(x) = $- y) \<longleftrightarrow> (intify(y) = $- x)"
 apply (cut_tac x = "intify (x) " and y = "intify (y) " in equation_zminus)
 apply auto
 done
 
-lemma zminus_equation_intify: "($- x = intify(y)) <-> ($- y = intify(x))"
+lemma zminus_equation_intify: "($- x = intify(y)) \<longleftrightarrow> ($- y = intify(x))"
 apply (cut_tac x = "intify (x) " and y = "intify (y) " in zminus_equation)
 apply auto
 done
@@ -914,16 +914,16 @@
 
 subsubsection{*The next several equations are permutative: watch out!*}
 
-lemma zless_zminus: "(x $< $- y) <-> (y $< $- x)"
+lemma zless_zminus: "(x $< $- y) \<longleftrightarrow> (y $< $- x)"
 by (simp add: zless_def zdiff_def zadd_ac)
 
-lemma zminus_zless: "($- x $< y) <-> ($- y $< x)"
+lemma zminus_zless: "($- x $< y) \<longleftrightarrow> ($- y $< x)"
 by (simp add: zless_def zdiff_def zadd_ac)
 
-lemma zle_zminus: "(x $<= $- y) <-> (y $<= $- x)"
+lemma zle_zminus: "(x $<= $- y) \<longleftrightarrow> (y $<= $- x)"
 by (simp add: not_zless_iff_zle [THEN iff_sym] zminus_zless)
 
-lemma zminus_zle: "($- x $<= y) <-> ($- y $<= x)"
+lemma zminus_zle: "($- x $<= y) \<longleftrightarrow> ($- y $<= x)"
 by (simp add: not_zless_iff_zle [THEN iff_sym] zless_zminus)
 
 end
diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/List_ZF.thy
--- a/src/ZF/List_ZF.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/List_ZF.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -136,11 +136,11 @@
 (*An elimination rule, for type-checking*)
 inductive_cases ConsE: "Cons(a,l) \<in> list(A)"
 
-lemma Cons_type_iff [simp]: "Cons(a,l) \<in> list(A) <-> a \<in> A & l \<in> list(A)"
+lemma Cons_type_iff [simp]: "Cons(a,l) \<in> list(A) \<longleftrightarrow> a \<in> A & l \<in> list(A)"
 by (blast elim: ConsE)
 
 (*Proving freeness results*)
-lemma Cons_iff: "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'"
+lemma Cons_iff: "Cons(a,l)=Cons(a',l') \<longleftrightarrow> a=a' & l=l'"
 by auto
 
 lemma Nil_Cons_iff: "~ Nil=Cons(a,l)"
@@ -480,7 +480,7 @@
 apply (auto dest: not_lt_imp_le)
 done
 
-lemma lt_min_iff: "[| i:nat; j:nat; k:nat |] ==> i<min(j,k) <-> i<j & i<k"
+lemma lt_min_iff: "[| i:nat; j:nat; k:nat |] ==> i<min(j,k) \<longleftrightarrow> i<j & i<k"
 apply (unfold min_def)
 apply (auto dest!: not_lt_imp_le intro: lt_trans2 lt_trans)
 done
@@ -518,43 +518,43 @@
 
 (** length **)
 
-lemma length_is_0_iff [simp]: "xs:list(A) ==> length(xs)=0 <-> xs=Nil"
+lemma length_is_0_iff [simp]: "xs:list(A) ==> length(xs)=0 \<longleftrightarrow> xs=Nil"
 by (erule list.induct, auto)
 
-lemma length_is_0_iff2 [simp]: "xs:list(A) ==> 0 = length(xs) <-> xs=Nil"
+lemma length_is_0_iff2 [simp]: "xs:list(A) ==> 0 = length(xs) \<longleftrightarrow> xs=Nil"
 by (erule list.induct, auto)
 
 lemma length_tl [simp]: "xs:list(A) ==> length(tl(xs)) = length(xs) #- 1"
 by (erule list.induct, auto)
 
-lemma length_greater_0_iff: "xs:list(A) ==> 0<length(xs) <-> xs \<noteq> Nil"
+lemma length_greater_0_iff: "xs:list(A) ==> 0<length(xs) \<longleftrightarrow> xs \<noteq> Nil"
 by (erule list.induct, auto)
 
-lemma length_succ_iff: "xs:list(A) ==> length(xs)=succ(n) <-> (\<exists>y ys. xs=Cons(y, ys) & length(ys)=n)"
+lemma length_succ_iff: "xs:list(A) ==> length(xs)=succ(n) \<longleftrightarrow> (\<exists>y ys. xs=Cons(y, ys) & length(ys)=n)"
 by (erule list.induct, auto)
 
 (** more theorems about append **)
 
 lemma append_is_Nil_iff [simp]:
-     "xs:list(A) ==> (xs@ys = Nil) <-> (xs=Nil & ys = Nil)"
+     "xs:list(A) ==> (xs@ys = Nil) \<longleftrightarrow> (xs=Nil & ys = Nil)"
 by (erule list.induct, auto)
 
 lemma append_is_Nil_iff2 [simp]:
-     "xs:list(A) ==> (Nil = xs@ys) <-> (xs=Nil & ys = Nil)"
+     "xs:list(A) ==> (Nil = xs@ys) \<longleftrightarrow> (xs=Nil & ys = Nil)"
 by (erule list.induct, auto)
 
 lemma append_left_is_self_iff [simp]:
-     "xs:list(A) ==> (xs@ys = xs) <-> (ys = Nil)"
+     "xs:list(A) ==> (xs@ys = xs) \<longleftrightarrow> (ys = Nil)"
 by (erule list.induct, auto)
 
 lemma append_left_is_self_iff2 [simp]:
-     "xs:list(A) ==> (xs = xs@ys) <-> (ys = Nil)"
+     "xs:list(A) ==> (xs = xs@ys) \<longleftrightarrow> (ys = Nil)"
 by (erule list.induct, auto)
 
 (*TOO SLOW as a default simprule!*)
 lemma append_left_is_Nil_iff [rule_format]:
      "[| xs:list(A); ys:list(A); zs:list(A) |] ==>
-   length(ys)=length(zs) \<longrightarrow> (xs@ys=zs <-> (xs=Nil & ys=zs))"
+   length(ys)=length(zs) \<longrightarrow> (xs@ys=zs \<longleftrightarrow> (xs=Nil & ys=zs))"
 apply (erule list.induct)
 apply (auto simp add: length_app)
 done
@@ -562,14 +562,14 @@
 (*TOO SLOW as a default simprule!*)
 lemma append_left_is_Nil_iff2 [rule_format]:
      "[| xs:list(A); ys:list(A); zs:list(A) |] ==>
-   length(ys)=length(zs) \<longrightarrow> (zs=ys@xs <-> (xs=Nil & ys=zs))"
+   length(ys)=length(zs) \<longrightarrow> (zs=ys@xs \<longleftrightarrow> (xs=Nil & ys=zs))"
 apply (erule list.induct)
 apply (auto simp add: length_app)
 done
 
 lemma append_eq_append_iff [rule_format,simp]:
      "xs:list(A) ==> \<forall>ys \<in> list(A).
-      length(xs)=length(ys) \<longrightarrow> (xs@us = ys@vs) <-> (xs=ys & us=vs)"
+      length(xs)=length(ys) \<longrightarrow> (xs@us = ys@vs) \<longleftrightarrow> (xs=ys & us=vs)"
 apply (erule list.induct)
 apply (simp (no_asm_simp))
 apply clarify
@@ -589,23 +589,23 @@
 
 lemma append_eq_append_iff2 [simp]:
  "[| xs:list(A); ys:list(A); us:list(A); vs:list(A); length(us)=length(vs) |]
-  ==>  xs@us = ys@vs <-> (xs=ys & us=vs)"
+  ==>  xs@us = ys@vs \<longleftrightarrow> (xs=ys & us=vs)"
 apply (rule iffI)
 apply (rule append_eq_append, auto)
 done
 
 lemma append_self_iff [simp]:
-     "[| xs:list(A); ys:list(A); zs:list(A) |] ==> xs@ys=xs@zs <-> ys=zs"
+     "[| xs:list(A); ys:list(A); zs:list(A) |] ==> xs@ys=xs@zs \<longleftrightarrow> ys=zs"
 by simp
 
 lemma append_self_iff2 [simp]:
-     "[| xs:list(A); ys:list(A); zs:list(A) |] ==> ys@xs=zs@xs <-> ys=zs"
+     "[| xs:list(A); ys:list(A); zs:list(A) |] ==> ys@xs=zs@xs \<longleftrightarrow> ys=zs"
 by simp
 
 (* Can also be proved from append_eq_append_iff2,
 but the proof requires two more hypotheses: x:A and y:A *)
 lemma append1_eq_iff [rule_format,simp]:
-     "xs:list(A) ==> \<forall>ys \<in> list(A). xs@[x] = ys@[y] <-> (xs = ys & x=y)"
+     "xs:list(A) ==> \<forall>ys \<in> list(A). xs@[x] = ys@[y] \<longleftrightarrow> (xs = ys & x=y)"
 apply (erule list.induct)
  apply clarify
  apply (erule list.cases)
@@ -617,11 +617,11 @@
 
 
 lemma append_right_is_self_iff [simp]:
-     "[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) <-> (xs=Nil)"
+     "[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) \<longleftrightarrow> (xs=Nil)"
 by (simp (no_asm_simp) add: append_left_is_Nil_iff)
 
 lemma append_right_is_self_iff2 [simp]:
-     "[| xs:list(A); ys:list(A) |] ==> (ys = xs@ys) <-> (xs=Nil)"
+     "[| xs:list(A); ys:list(A) |] ==> (ys = xs@ys) \<longleftrightarrow> (xs=Nil)"
 apply (rule iffI)
 apply (drule sym, auto)
 done
@@ -635,14 +635,14 @@
 by (induct_tac "xs", auto)
 
 (** rev **)
-lemma rev_is_Nil_iff [simp]: "xs:list(A) ==> (rev(xs) = Nil <-> xs = Nil)"
+lemma rev_is_Nil_iff [simp]: "xs:list(A) ==> (rev(xs) = Nil \<longleftrightarrow> xs = Nil)"
 by (erule list.induct, auto)
 
-lemma Nil_is_rev_iff [simp]: "xs:list(A) ==> (Nil = rev(xs) <-> xs = Nil)"
+lemma Nil_is_rev_iff [simp]: "xs:list(A) ==> (Nil = rev(xs) \<longleftrightarrow> xs = Nil)"
 by (erule list.induct, auto)
 
 lemma rev_is_rev_iff [rule_format,simp]:
-     "xs:list(A) ==> \<forall>ys \<in> list(A). rev(xs)=rev(ys) <-> xs=ys"
+     "xs:list(A) ==> \<forall>ys \<in> list(A). rev(xs)=rev(ys) \<longleftrightarrow> xs=ys"
 apply (erule list.induct, force, clarify)
 apply (erule_tac a = ys in list.cases, auto)
 done
@@ -1027,7 +1027,7 @@
 lemma list_update_same_conv [rule_format]:
      "xs:list(A) ==>
       \<forall>i \<in> nat. i < length(xs) \<longrightarrow>
-                 (list_update(xs, i, x) = xs) <-> (nth(i, xs) = x)"
+                 (list_update(xs, i, x) = xs) \<longleftrightarrow> (nth(i, xs) = x)"
 apply (induct_tac "xs")
  apply (simp (no_asm))
 apply clarify
diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/Nat_ZF.thy
--- a/src/ZF/Nat_ZF.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Nat_ZF.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -123,7 +123,7 @@
 lemma succ_natD: "succ(i): nat ==> i: nat"
 by (rule Ord_trans [OF succI1], auto)
 
-lemma nat_succ_iff [iff]: "succ(n): nat <-> n: nat"
+lemma nat_succ_iff [iff]: "succ(n): nat \<longleftrightarrow> n: nat"
 by (blast dest!: succ_natD)
 
 lemma nat_le_Limit: "Limit(i) ==> nat \<le> i"
@@ -246,7 +246,7 @@
 by (erule nat_induct, auto)
 
 lemma split_nat_case:
-  "P(nat_case(a,b,k)) <->
+  "P(nat_case(a,b,k)) \<longleftrightarrow>
    ((k=0 \<longrightarrow> P(a)) & (\<forall>x. k=succ(x) \<longrightarrow> P(b(x))) & (~ quasinat(k) \<longrightarrow> P(0)))"
 apply (rule nat_cases [of k])
 apply (auto simp add: non_nat_case)
@@ -294,7 +294,7 @@
 apply (blast intro: lt_trans)
 done
 
-lemma Le_iff [iff]: "<x,y> \<in> Le <-> x \<le> y & x \<in> nat & y \<in> nat"
+lemma Le_iff [iff]: "<x,y> \<in> Le \<longleftrightarrow> x \<le> y & x \<in> nat & y \<in> nat"
 by (force simp add: Le_def)
 
 end
diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/Order.thy
--- a/src/ZF/Order.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Order.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -51,7 +51,7 @@
 definition
   ord_iso  :: "[i,i,i,i]=>i"            (*Order isomorphisms*)  where
    "ord_iso(A,r,B,s) ==
-              {f: bij(A,B). \<forall>x\<in>A. \<forall>y\<in>A. <x,y>:r <-> <f`x,f`y>:s}"
+              {f: bij(A,B). \<forall>x\<in>A. \<forall>y\<in>A. <x,y>:r \<longleftrightarrow> <f`x,f`y>:s}"
 
 definition
   pred     :: "[i,i,i]=>i"              (*Set of predecessors*)  where
@@ -107,7 +107,7 @@
 
 (** Derived rules for pred(A,x,r) **)
 
-lemma pred_iff: "y \<in> pred(A,x,r) <-> <y,x>:r & y:A"
+lemma pred_iff: "y \<in> pred(A,x,r) \<longleftrightarrow> <y,x>:r & y:A"
 by (unfold pred_def, blast)
 
 lemmas predI = conjI [THEN pred_iff [THEN iffD2]]
@@ -160,30 +160,30 @@
 
 (** Relations restricted to a smaller domain, by Krzysztof Grabczewski **)
 
-lemma irrefl_Int_iff: "irrefl(A,r \<inter> A*A) <-> irrefl(A,r)"
+lemma irrefl_Int_iff: "irrefl(A,r \<inter> A*A) \<longleftrightarrow> irrefl(A,r)"
 by (unfold irrefl_def, blast)
 
-lemma trans_on_Int_iff: "trans[A](r \<inter> A*A) <-> trans[A](r)"
+lemma trans_on_Int_iff: "trans[A](r \<inter> A*A) \<longleftrightarrow> trans[A](r)"
 by (unfold trans_on_def, blast)
 
-lemma part_ord_Int_iff: "part_ord(A,r \<inter> A*A) <-> part_ord(A,r)"
+lemma part_ord_Int_iff: "part_ord(A,r \<inter> A*A) \<longleftrightarrow> part_ord(A,r)"
 apply (unfold part_ord_def)
 apply (simp add: irrefl_Int_iff trans_on_Int_iff)
 done
 
-lemma linear_Int_iff: "linear(A,r \<inter> A*A) <-> linear(A,r)"
+lemma linear_Int_iff: "linear(A,r \<inter> A*A) \<longleftrightarrow> linear(A,r)"
 by (unfold linear_def, blast)
 
-lemma tot_ord_Int_iff: "tot_ord(A,r \<inter> A*A) <-> tot_ord(A,r)"
+lemma tot_ord_Int_iff: "tot_ord(A,r \<inter> A*A) \<longleftrightarrow> tot_ord(A,r)"
 apply (unfold tot_ord_def)
 apply (simp add: part_ord_Int_iff linear_Int_iff)
 done
 
-lemma wf_on_Int_iff: "wf[A](r \<inter> A*A) <-> wf[A](r)"
+lemma wf_on_Int_iff: "wf[A](r \<inter> A*A) \<longleftrightarrow> wf[A](r)"
 apply (unfold wf_on_def wf_def, fast) (*10 times faster than blast!*)
 done
 
-lemma well_ord_Int_iff: "well_ord(A,r \<inter> A*A) <-> well_ord(A,r)"
+lemma well_ord_Int_iff: "well_ord(A,r \<inter> A*A) \<longleftrightarrow> well_ord(A,r)"
 apply (unfold well_ord_def)
 apply (simp add: tot_ord_Int_iff wf_on_Int_iff)
 done
@@ -256,7 +256,7 @@
 
 lemma ord_isoI:
     "[| f: bij(A, B);
-        !!x y. [| x:A; y:A |] ==> <x, y> \<in> r <-> <f`x, f`y> \<in> s |]
+        !!x y. [| x:A; y:A |] ==> <x, y> \<in> r \<longleftrightarrow> <f`x, f`y> \<in> s |]
      ==> f: ord_iso(A,r,B,s)"
 by (simp add: ord_iso_def)
 
@@ -666,7 +666,7 @@
 
 lemma subset_vimage_vimage_iff:
   "[| Preorder(r); A \<subseteq> field(r); B \<subseteq> field(r) |] ==>
-  r -`` A \<subseteq> r -`` B <-> (\<forall>a\<in>A. \<exists>b\<in>B. <a, b> \<in> r)"
+  r -`` A \<subseteq> r -`` B \<longleftrightarrow> (\<forall>a\<in>A. \<exists>b\<in>B. <a, b> \<in> r)"
   apply (auto simp: subset_def preorder_on_def refl_def vimage_def image_def)
    apply blast
   unfolding trans_on_def
@@ -679,12 +679,12 @@
 
 lemma subset_vimage1_vimage1_iff:
   "[| Preorder(r); a \<in> field(r); b \<in> field(r) |] ==>
-  r -`` {a} \<subseteq> r -`` {b} <-> <a, b> \<in> r"
+  r -`` {a} \<subseteq> r -`` {b} \<longleftrightarrow> <a, b> \<in> r"
   by (simp add: subset_vimage_vimage_iff)
 
 lemma Refl_antisym_eq_Image1_Image1_iff:
   "[| refl(field(r), r); antisym(r); a \<in> field(r); b \<in> field(r) |] ==>
-  r `` {a} = r `` {b} <-> a = b"
+  r `` {a} = r `` {b} \<longleftrightarrow> a = b"
   apply rule
    apply (frule equality_iffD)
    apply (drule equality_iffD)
@@ -695,13 +695,13 @@
 
 lemma Partial_order_eq_Image1_Image1_iff:
   "[| Partial_order(r); a \<in> field(r); b \<in> field(r) |] ==>
-  r `` {a} = r `` {b} <-> a = b"
+  r `` {a} = r `` {b} \<longleftrightarrow> a = b"
   by (simp add: partial_order_on_def preorder_on_def
     Refl_antisym_eq_Image1_Image1_iff)
 
 lemma Refl_antisym_eq_vimage1_vimage1_iff:
   "[| refl(field(r), r); antisym(r); a \<in> field(r); b \<in> field(r) |] ==>
-  r -`` {a} = r -`` {b} <-> a = b"
+  r -`` {a} = r -`` {b} \<longleftrightarrow> a = b"
   apply rule
    apply (frule equality_iffD)
    apply (drule equality_iffD)
@@ -712,7 +712,7 @@
 
 lemma Partial_order_eq_vimage1_vimage1_iff:
   "[| Partial_order(r); a \<in> field(r); b \<in> field(r) |] ==>
-  r -`` {a} = r -`` {b} <-> a = b"
+  r -`` {a} = r -`` {b} \<longleftrightarrow> a = b"
   by (simp add: partial_order_on_def preorder_on_def
     Refl_antisym_eq_vimage1_vimage1_iff)
 
diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/OrderArith.thy
--- a/src/ZF/OrderArith.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/OrderArith.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -39,19 +39,19 @@
 subsubsection{*Rewrite rules.  Can be used to obtain introduction rules*}
 
 lemma radd_Inl_Inr_iff [iff]: 
-    "<Inl(a), Inr(b)> \<in> radd(A,r,B,s)  <->  a:A & b:B"
+    "<Inl(a), Inr(b)> \<in> radd(A,r,B,s)  \<longleftrightarrow>  a:A & b:B"
 by (unfold radd_def, blast)
 
 lemma radd_Inl_iff [iff]: 
-    "<Inl(a'), Inl(a)> \<in> radd(A,r,B,s)  <->  a':A & a:A & <a',a>:r"
+    "<Inl(a'), Inl(a)> \<in> radd(A,r,B,s)  \<longleftrightarrow>  a':A & a:A & <a',a>:r"
 by (unfold radd_def, blast)
 
 lemma radd_Inr_iff [iff]: 
-    "<Inr(b'), Inr(b)> \<in> radd(A,r,B,s) <->  b':B & b:B & <b',b>:s"
+    "<Inr(b'), Inr(b)> \<in> radd(A,r,B,s) \<longleftrightarrow>  b':B & b:B & <b',b>:s"
 by (unfold radd_def, blast)
 
 lemma radd_Inr_Inl_iff [simp]: 
-    "<Inr(b), Inl(a)> \<in> radd(A,r,B,s) <-> False"
+    "<Inr(b), Inl(a)> \<in> radd(A,r,B,s) \<longleftrightarrow> False"
 by (unfold radd_def, blast)
 
 declare radd_Inr_Inl_iff [THEN iffD1, dest!] 
@@ -163,7 +163,7 @@
 subsubsection{*Rewrite rule.  Can be used to obtain introduction rules*}
 
 lemma  rmult_iff [iff]: 
-    "<<a',b'>, <a,b>> \<in> rmult(A,r,B,s) <->        
+    "<<a',b'>, <a,b>> \<in> rmult(A,r,B,s) \<longleftrightarrow>        
             (<a',a>: r  & a':A & a:A & b': B & b: B) |   
             (<b',b>: s  & a'=a & a:A & b': B & b: B)"
 
@@ -307,7 +307,7 @@
 
 subsubsection{*Rewrite rule*}
 
-lemma rvimage_iff: "<a,b> \<in> rvimage(A,f,r)  <->  <f`a,f`b>: r & a:A & b:A"
+lemma rvimage_iff: "<a,b> \<in> rvimage(A,f,r)  \<longleftrightarrow>  <f`a,f`b>: r & a:A & b:A"
 by (unfold rvimage_def, blast)
 
 subsubsection{*Type checking*}
@@ -450,7 +450,7 @@
 done
 
 theorem wf_iff_subset_rvimage:
-  "relation(r) ==> wf(r) <-> (\<exists>i f A. Ord(i) & r \<subseteq> rvimage(A, f, Memrel(i)))"
+  "relation(r) ==> wf(r) \<longleftrightarrow> (\<exists>i f A. Ord(i) & r \<subseteq> rvimage(A, f, Memrel(i)))"
 by (blast dest!: relation_field_times_field wf_imp_subset_rvimage
           intro: wf_rvimage_Ord [THEN wf_subset])
 
@@ -496,7 +496,7 @@
 lemma wf_measure [iff]: "wf(measure(A,f))"
 by (simp (no_asm) add: measure_eq_rvimage_Memrel wf_Memrel wf_rvimage)
 
-lemma measure_iff [iff]: "<x,y> \<in> measure(A,f) <-> x:A & y:A & f(x)<f(y)"
+lemma measure_iff [iff]: "<x,y> \<in> measure(A,f) \<longleftrightarrow> x:A & y:A & f(x)<f(y)"
 by (simp (no_asm) add: measure_def)
 
 lemma linear_measure: 
diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/OrderType.thy
--- a/src/ZF/OrderType.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/OrderType.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -533,7 +533,7 @@
 apply (blast dest: oadd_lt_mono2 elim: lt_irrefl lt_asym)+
 done
 
-lemma oadd_lt_iff2: "Ord(j) ==> i++j < i++k <-> j<k"
+lemma oadd_lt_iff2: "Ord(j) ==> i++j < i++k \<longleftrightarrow> j<k"
 by (blast intro!: oadd_lt_mono2 dest!: oadd_lt_cancel2)
 
 lemma oadd_inject: "[| i++j = i++k;  Ord(j); Ord(k) |] ==> j=k"
@@ -607,13 +607,13 @@
                  Union_eq_UN [symmetric] Limit_Union_eq)
 done
 
-lemma oadd_eq_0_iff: "[| Ord(i); Ord(j) |] ==> (i ++ j) = 0 <-> i=0 & j=0"
+lemma oadd_eq_0_iff: "[| Ord(i); Ord(j) |] ==> (i ++ j) = 0 \<longleftrightarrow> i=0 & j=0"
 apply (erule trans_induct3 [of j])
 apply (simp_all add: oadd_Limit)
 apply (simp add: Union_empty_iff Limit_def lt_def, blast)
 done
 
-lemma oadd_eq_lt_iff: "[| Ord(i); Ord(j) |] ==> 0 < (i ++ j) <-> 0<i | 0<j"
+lemma oadd_eq_lt_iff: "[| Ord(i); Ord(j) |] ==> 0 < (i ++ j) \<longleftrightarrow> 0<i | 0<j"
 by (simp add: Ord_0_lt_iff [symmetric] oadd_eq_0_iff)
 
 lemma oadd_LimitI: "[| Ord(i); Limit(j) |] ==> Limit(i ++ j)"
@@ -661,7 +661,7 @@
 lemma oadd_le_mono: "[| i' \<le> i;  j' \<le> j |] ==> i'++j' \<le> i++j"
 by (simp del: oadd_succ add: oadd_succ [symmetric] le_Ord2 oadd_lt_mono)
 
-lemma oadd_le_iff2: "[| Ord(j); Ord(k) |] ==> i++j \<le> i++k <-> j \<le> k"
+lemma oadd_le_iff2: "[| Ord(j); Ord(k) |] ==> i++j \<le> i++k \<longleftrightarrow> j \<le> k"
 by (simp del: oadd_succ add: oadd_lt_iff2 oadd_succ [symmetric] Ord_succ)
 
 lemma oadd_lt_self: "[| Ord(i);  0<j |] ==> i < i++j"
diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/Perm.thy
--- a/src/ZF/Perm.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Perm.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -15,7 +15,7 @@
 definition
   (*composition of relations and functions; NOT Suppes's relative product*)
   comp     :: "[i,i]=>i"      (infixr "O" 60)  where
-    "r O s == {xz \<in> domain(s)*range(r) . 
+    "r O s == {xz \<in> domain(s)*range(r) .
                \<exists>x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
 
 definition
@@ -58,17 +58,17 @@
 
 text{* A function with a right inverse is a surjection *}
 
-lemma f_imp_surjective: 
+lemma f_imp_surjective:
     "[| f: A->B;  !!y. y:B ==> d(y): A;  !!y. y:B ==> f`d(y) = y |]
      ==> f: surj(A,B)"
   by (simp add: surj_def, blast)
 
-lemma lam_surjective: 
-    "[| !!x. x:A ==> c(x): B;            
-        !!y. y:B ==> d(y): A;            
-        !!y. y:B ==> c(d(y)) = y         
+lemma lam_surjective:
+    "[| !!x. x:A ==> c(x): B;
+        !!y. y:B ==> d(y): A;
+        !!y. y:B ==> c(d(y)) = y
      |] ==> (\<lambda>x\<in>A. c(x)) \<in> surj(A,B)"
-apply (rule_tac d = d in f_imp_surjective) 
+apply (rule_tac d = d in f_imp_surjective)
 apply (simp_all add: lam_type)
 done
 
@@ -76,7 +76,7 @@
 lemma cantor_surj: "f \<notin> surj(A,Pow(A))"
 apply (unfold surj_def, safe)
 apply (cut_tac cantor)
-apply (best del: subsetI) 
+apply (best del: subsetI)
 done
 
 
@@ -88,7 +88,7 @@
 done
 
 text{*Good for dealing with sets of pairs, but a bit ugly in use [used in AC]*}
-lemma inj_equality: 
+lemma inj_equality:
     "[| <a,b>:f;  <c,b>:f;  f: inj(A,B) |] ==> a=c"
 apply (unfold inj_def)
 apply (blast dest: Pair_mem_PiD)
@@ -104,8 +104,8 @@
 apply (blast intro: subst_context [THEN box_equals])
 done
 
-lemma lam_injective: 
-    "[| !!x. x:A ==> c(x): B;            
+lemma lam_injective:
+    "[| !!x. x:A ==> c(x): B;
         !!x. x:A ==> d(c(x)) = x |]
      ==> (\<lambda>x\<in>A. c(x)) \<in> inj(A,B)"
 apply (rule_tac d = d in f_imp_injective)
@@ -127,17 +127,17 @@
 text{* f: bij(A,B) ==> f: A->B *}
 lemmas bij_is_fun = bij_is_inj [THEN inj_is_fun]
 
-lemma lam_bijective: 
-    "[| !!x. x:A ==> c(x): B;            
-        !!y. y:B ==> d(y): A;            
-        !!x. x:A ==> d(c(x)) = x;        
-        !!y. y:B ==> c(d(y)) = y         
+lemma lam_bijective:
+    "[| !!x. x:A ==> c(x): B;
+        !!y. y:B ==> d(y): A;
+        !!x. x:A ==> d(c(x)) = x;
+        !!y. y:B ==> c(d(y)) = y
      |] ==> (\<lambda>x\<in>A. c(x)) \<in> bij(A,B)"
 apply (unfold bij_def)
 apply (blast intro!: lam_injective lam_surjective)
 done
 
-lemma RepFun_bijective: "(\<forall>y\<in>x. EX! y'. f(y') = f(y))   
+lemma RepFun_bijective: "(\<forall>y\<in>x. EX! y'. f(y') = f(y))
       ==> (\<lambda>z\<in>{f(y). y:x}. THE y. f(y) = z) \<in> bij({f(y). y:x}, x)"
 apply (rule_tac d = f in lam_bijective)
 apply (auto simp add: the_equality2)
@@ -171,7 +171,7 @@
 
 lemma id_subset_inj: "A<=B ==> id(A): inj(A,B)"
 apply (simp add: inj_def id_def)
-apply (blast intro: lam_type) 
+apply (blast intro: lam_type)
 done
 
 lemmas id_inj = subset_refl [THEN id_subset_inj]
@@ -186,13 +186,13 @@
 apply (blast intro: id_inj id_surj)
 done
 
-lemma subset_iff_id: "A \<subseteq> B <-> id(A) \<in> A->B"
+lemma subset_iff_id: "A \<subseteq> B \<longleftrightarrow> id(A) \<in> A->B"
 apply (unfold id_def)
 apply (force intro!: lam_type dest: apply_type)
 done
 
 text{*@{term id} as the identity relation*}
-lemma id_iff [simp]: "<x,y> \<in> id(A) <-> x=y & y \<in> A"
+lemma id_iff [simp]: "<x,y> \<in> id(A) \<longleftrightarrow> x=y & y \<in> A"
 by auto
 
 
@@ -224,7 +224,7 @@
 
 lemma right_inverse_lemma:
      "[| f: A->B;  converse(f): C->A;  b: C |] ==> f`(converse(f)`b) = b"
-by (rule apply_Pair [THEN converseD [THEN apply_equality]], auto) 
+by (rule apply_Pair [THEN converseD [THEN apply_equality]], auto)
 
 (*Should the premises be f:surj(A,B), b:B for symmetry with left_inverse?
   No: they would not imply that converse(f) was a function! *)
@@ -239,14 +239,14 @@
 
 lemma inj_converse_inj: "f: inj(A,B) ==> converse(f): inj(range(f), A)"
 apply (rule f_imp_injective)
-apply (erule inj_converse_fun, clarify) 
+apply (erule inj_converse_fun, clarify)
 apply (rule right_inverse)
  apply assumption
-apply blast 
+apply blast
 done
 
 lemma inj_converse_surj: "f: inj(A,B) ==> converse(f): surj(range(f), A)"
-by (blast intro: f_imp_surjective inj_converse_fun left_inverse inj_is_fun 
+by (blast intro: f_imp_surjective inj_converse_fun left_inverse inj_is_fun
                  range_of_fun [THEN apply_type])
 
 text{*Adding this as an intro! rule seems to cause looping*}
@@ -264,17 +264,17 @@
 lemma compI [intro]: "[| <a,b>:s; <b,c>:r |] ==> <a,c> \<in> r O s"
 by (unfold comp_def, blast)
 
-lemma compE [elim!]: 
-    "[| xz \<in> r O s;   
+lemma compE [elim!]:
+    "[| xz \<in> r O s;
         !!x y z. [| xz=<x,z>;  <x,y>:s;  <y,z>:r |] ==> P |]
      ==> P"
 by (unfold comp_def, blast)
 
-lemma compEpair: 
-    "[| <a,c> \<in> r O s;   
+lemma compEpair:
+    "[| <a,c> \<in> r O s;
         !!y. [| <a,y>:s;  <y,c>:r |] ==> P |]
      ==> P"
-by (erule compE, simp)  
+by (erule compE, simp)
 
 lemma converse_comp: "converse(R O S) = converse(S) O converse(R)"
 by blast
@@ -302,7 +302,7 @@
   by (auto simp add: inj_def Pi_iff function_def)
 
 lemma inj_bij_range: "f: inj(A,B) ==> f \<in> bij(A,range(f))"
-  by (auto simp add: bij_def intro: inj_inj_range inj_is_fun fun_is_surj) 
+  by (auto simp add: bij_def intro: inj_inj_range inj_is_fun fun_is_surj)
 
 
 subsection{*Other Results*}
@@ -319,7 +319,7 @@
 by blast
 
 (*left identity of composition; provable inclusions are
-        id(A) O r \<subseteq> r       
+        id(A) O r \<subseteq> r
   and   [| r<=A*B; B<=C |] ==> r \<subseteq> id(C) O r *)
 lemma left_comp_id: "r<=A*B ==> id(B) O r = r"
 by blast
@@ -339,44 +339,44 @@
 text{*Don't think the premises can be weakened much*}
 lemma comp_fun: "[| g: A->B;  f: B->C |] ==> (f O g) \<in> A->C"
 apply (auto simp add: Pi_def comp_function Pow_iff comp_rel)
-apply (subst range_rel_subset [THEN domain_comp_eq], auto) 
+apply (subst range_rel_subset [THEN domain_comp_eq], auto)
 done
 
 (*Thanks to the new definition of "apply", the premise f: B->C is gone!*)
 lemma comp_fun_apply [simp]:
      "[| g: A->B;  a:A |] ==> (f O g)`a = f`(g`a)"
-apply (frule apply_Pair, assumption) 
+apply (frule apply_Pair, assumption)
 apply (simp add: apply_def image_comp)
-apply (blast dest: apply_equality) 
+apply (blast dest: apply_equality)
 done
 
 text{*Simplifies compositions of lambda-abstractions*}
-lemma comp_lam: 
+lemma comp_lam:
     "[| !!x. x:A ==> b(x): B |]
      ==> (\<lambda>y\<in>B. c(y)) O (\<lambda>x\<in>A. b(x)) = (\<lambda>x\<in>A. c(b(x)))"
-apply (subgoal_tac "(\<lambda>x\<in>A. b(x)) \<in> A -> B") 
+apply (subgoal_tac "(\<lambda>x\<in>A. b(x)) \<in> A -> B")
  apply (rule fun_extension)
    apply (blast intro: comp_fun lam_funtype)
   apply (rule lam_funtype)
- apply simp 
-apply (simp add: lam_type) 
+ apply simp
+apply (simp add: lam_type)
 done
 
 lemma comp_inj:
      "[| g: inj(A,B);  f: inj(B,C) |] ==> (f O g) \<in> inj(A,C)"
-apply (frule inj_is_fun [of g]) 
-apply (frule inj_is_fun [of f]) 
+apply (frule inj_is_fun [of g])
+apply (frule inj_is_fun [of f])
 apply (rule_tac d = "%y. converse (g) ` (converse (f) ` y)" in f_imp_injective)
- apply (blast intro: comp_fun, simp)  
+ apply (blast intro: comp_fun, simp)
 done
 
-lemma comp_surj: 
+lemma comp_surj:
     "[| g: surj(A,B);  f: surj(B,C) |] ==> (f O g) \<in> surj(A,C)"
 apply (unfold surj_def)
 apply (blast intro!: comp_fun comp_fun_apply)
 done
 
-lemma comp_bij: 
+lemma comp_bij:
     "[| g: bij(A,B);  f: bij(B,C) |] ==> (f O g) \<in> bij(A,C)"
 apply (unfold bij_def)
 apply (blast intro: comp_inj comp_surj)
@@ -386,14 +386,14 @@
 subsection{*Dual Properties of @{term inj} and @{term surj}*}
 
 text{*Useful for proofs from
-    D Pastre.  Automatic theorem proving in set theory. 
+    D Pastre.  Automatic theorem proving in set theory.
     Artificial Intelligence, 10:1--27, 1978.*}
 
-lemma comp_mem_injD1: 
+lemma comp_mem_injD1:
     "[| (f O g): inj(A,C);  g: A->B;  f: B->C |] ==> g: inj(A,B)"
-by (unfold inj_def, force) 
+by (unfold inj_def, force)
 
-lemma comp_mem_injD2: 
+lemma comp_mem_injD2:
     "[| (f O g): inj(A,C);  g: surj(A,B);  f: B->C |] ==> f: inj(B,C)"
 apply (unfold inj_def surj_def, safe)
 apply (rule_tac x1 = x in bspec [THEN bexE])
@@ -403,17 +403,17 @@
 apply (simp (no_asm_simp))
 done
 
-lemma comp_mem_surjD1: 
+lemma comp_mem_surjD1:
     "[| (f O g): surj(A,C);  g: A->B;  f: B->C |] ==> f: surj(B,C)"
 apply (unfold surj_def)
 apply (blast intro!: comp_fun_apply [symmetric] apply_funtype)
 done
 
 
-lemma comp_mem_surjD2: 
+lemma comp_mem_surjD2:
     "[| (f O g): surj(A,C);  g: A->B;  f: inj(B,C) |] ==> g: surj(A,B)"
 apply (unfold inj_def surj_def, safe)
-apply (drule_tac x = "f`y" in bspec, auto)  
+apply (drule_tac x = "f`y" in bspec, auto)
 apply (blast intro: apply_funtype)
 done
 
@@ -422,16 +422,16 @@
 text{*left inverse of composition; one inclusion is
         @{term "f: A->B ==> id(A) \<subseteq> converse(f) O f"} *}
 lemma left_comp_inverse: "f: inj(A,B) ==> converse(f) O f = id(A)"
-apply (unfold inj_def, clarify) 
-apply (rule equalityI) 
- apply (auto simp add: apply_iff, blast)  
+apply (unfold inj_def, clarify)
+apply (rule equalityI)
+ apply (auto simp add: apply_iff, blast)
 done
 
 text{*right inverse of composition; one inclusion is
                 @{term "f: A->B ==> f O converse(f) \<subseteq> id(B)"} *}
-lemma right_comp_inverse: 
+lemma right_comp_inverse:
     "f: surj(A,B) ==> f O converse(f) = id(B)"
-apply (simp add: surj_def, clarify) 
+apply (simp add: surj_def, clarify)
 apply (rule equalityI)
 apply (best elim: domain_type range_type dest: apply_equality2)
 apply (blast intro: apply_Pair)
@@ -440,8 +440,8 @@
 
 subsubsection{*Proving that a Function is a Bijection*}
 
-lemma comp_eq_id_iff: 
-    "[| f: A->B;  g: B->A |] ==> f O g = id(B) <-> (\<forall>y\<in>B. f`(g`y)=y)"
+lemma comp_eq_id_iff:
+    "[| f: A->B;  g: B->A |] ==> f O g = id(B) \<longleftrightarrow> (\<forall>y\<in>B. f`(g`y)=y)"
 apply (unfold id_def, safe)
  apply (drule_tac t = "%h. h`y " in subst_context)
  apply simp
@@ -450,7 +450,7 @@
  apply auto
 done
 
-lemma fg_imp_bijective: 
+lemma fg_imp_bijective:
     "[| f: A->B;  g: B->A;  f O g = id(B);  g O f = id(A) |] ==> f \<in> bij(A,B)"
 apply (unfold bij_def)
 apply (simp add: comp_eq_id_iff)
@@ -462,7 +462,7 @@
 
 lemma invertible_imp_bijective:
      "[| converse(f): B->A;  f: A->B |] ==> f \<in> bij(A,B)"
-by (simp add: fg_imp_bijective comp_eq_id_iff 
+by (simp add: fg_imp_bijective comp_eq_id_iff
               left_inverse_lemma right_inverse_lemma)
 
 subsubsection{*Unions of Functions*}
@@ -471,25 +471,25 @@
 
 text{*Theorem by KG, proof by LCP*}
 lemma inj_disjoint_Un:
-     "[| f: inj(A,B);  g: inj(C,D);  B \<inter> D = 0 |]  
+     "[| f: inj(A,B);  g: inj(C,D);  B \<inter> D = 0 |]
       ==> (\<lambda>a\<in>A \<union> C. if a:A then f`a else g`a) \<in> inj(A \<union> C, B \<union> D)"
-apply (rule_tac d = "%z. if z:B then converse (f) `z else converse (g) `z" 
+apply (rule_tac d = "%z. if z:B then converse (f) `z else converse (g) `z"
        in lam_injective)
 apply (auto simp add: inj_is_fun [THEN apply_type])
 done
 
-lemma surj_disjoint_Un: 
-    "[| f: surj(A,B);  g: surj(C,D);  A \<inter> C = 0 |]   
+lemma surj_disjoint_Un:
+    "[| f: surj(A,B);  g: surj(C,D);  A \<inter> C = 0 |]
      ==> (f \<union> g) \<in> surj(A \<union> C, B \<union> D)"
-apply (simp add: surj_def fun_disjoint_Un) 
-apply (blast dest!: domain_of_fun 
+apply (simp add: surj_def fun_disjoint_Un)
+apply (blast dest!: domain_of_fun
              intro!: fun_disjoint_apply1 fun_disjoint_apply2)
 done
 
 text{*A simple, high-level proof; the version for injections follows from it,
-  using  @term{f:inj(A,B) <-> f:bij(A,range(f))}  *}
+  using  @{term "f:inj(A,B) \<longleftrightarrow> f:bij(A,range(f))"}  *}
 lemma bij_disjoint_Un:
-     "[| f: bij(A,B);  g: bij(C,D);  A \<inter> C = 0;  B \<inter> D = 0 |]  
+     "[| f: bij(A,B);  g: bij(C,D);  A \<inter> C = 0;  B \<inter> D = 0 |]
       ==> (f \<union> g) \<in> bij(A \<union> C, B \<union> D)"
 apply (rule invertible_imp_bijective)
 apply (subst converse_Un)
@@ -501,25 +501,25 @@
 
 lemma surj_image:
     "f: Pi(A,B) ==> f: surj(A, f``A)"
-apply (simp add: surj_def) 
-apply (blast intro: apply_equality apply_Pair Pi_type) 
+apply (simp add: surj_def)
+apply (blast intro: apply_equality apply_Pair Pi_type)
 done
 
 lemma restrict_image [simp]: "restrict(f,A) `` B = f `` (A \<inter> B)"
 by (auto simp add: restrict_def)
 
-lemma restrict_inj: 
+lemma restrict_inj:
     "[| f: inj(A,B);  C<=A |] ==> restrict(f,C): inj(C,B)"
 apply (unfold inj_def)
-apply (safe elim!: restrict_type2, auto) 
+apply (safe elim!: restrict_type2, auto)
 done
 
 lemma restrict_surj: "[| f: Pi(A,B);  C<=A |] ==> restrict(f,C): surj(C, f``C)"
 apply (insert restrict_type2 [THEN surj_image])
-apply (simp add: restrict_image) 
+apply (simp add: restrict_image)
 done
 
-lemma restrict_bij: 
+lemma restrict_bij:
     "[| f: inj(A,B);  C<=A |] ==> restrict(f,C): bij(C, f``C)"
 apply (simp add: inj_def bij_def)
 apply (blast intro: restrict_surj surj_is_fun)
@@ -541,8 +541,8 @@
 done
 
 
-lemma inj_extend: 
-    "[| f: inj(A,B);  a\<notin>A;  b\<notin>B |]  
+lemma inj_extend:
+    "[| f: inj(A,B);  a\<notin>A;  b\<notin>B |]
      ==> cons(<a,b>,f) \<in> inj(cons(a,A), cons(b,B))"
 apply (unfold inj_def)
 apply (force intro: apply_type  simp add: fun_extend)
diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/QPair.thy
--- a/src/ZF/QPair.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/QPair.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -77,7 +77,7 @@
 lemma QPair_empty [simp]: "<0;0> = 0"
 by (simp add: QPair_def)
 
-lemma QPair_iff [simp]: "<a;b> = <c;d> <-> a=c & b=d"
+lemma QPair_iff [simp]: "<a;b> = <c;d> \<longleftrightarrow> a=c & b=d"
 apply (simp add: QPair_def)
 apply (rule sum_equal_iff)
 done
@@ -160,7 +160,7 @@
 by auto 
 
 lemma expand_qsplit: 
- "u: A<*>B ==> R(qsplit(c,u)) <-> (\<forall>x\<in>A. \<forall>y\<in>B. u = <x;y> \<longrightarrow> R(c(x,y)))"
+ "u: A<*>B ==> R(qsplit(c,u)) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. u = <x;y> \<longrightarrow> R(c(x,y)))"
 apply (simp add: qsplit_def, auto)
 done
 
@@ -232,16 +232,16 @@
 
 (** Injection and freeness equivalences, for rewriting **)
 
-lemma QInl_iff [iff]: "QInl(a)=QInl(b) <-> a=b"
+lemma QInl_iff [iff]: "QInl(a)=QInl(b) \<longleftrightarrow> a=b"
 by (simp add: qsum_defs )
 
-lemma QInr_iff [iff]: "QInr(a)=QInr(b) <-> a=b"
+lemma QInr_iff [iff]: "QInr(a)=QInr(b) \<longleftrightarrow> a=b"
 by (simp add: qsum_defs )
 
-lemma QInl_QInr_iff [simp]: "QInl(a)=QInr(b) <-> False"
+lemma QInl_QInr_iff [simp]: "QInl(a)=QInr(b) \<longleftrightarrow> False"
 by (simp add: qsum_defs )
 
-lemma QInr_QInl_iff [simp]: "QInr(b)=QInl(a) <-> False"
+lemma QInr_QInl_iff [simp]: "QInr(b)=QInl(a) \<longleftrightarrow> False"
 by (simp add: qsum_defs )
 
 lemma qsum_empty [simp]: "0<+>0 = 0"
@@ -263,13 +263,13 @@
 (** <+> is itself injective... who cares?? **)
 
 lemma qsum_iff:
-     "u: A <+> B <-> (\<exists>x. x:A & u=QInl(x)) | (\<exists>y. y:B & u=QInr(y))"
+     "u: A <+> B \<longleftrightarrow> (\<exists>x. x:A & u=QInl(x)) | (\<exists>y. y:B & u=QInr(y))"
 by blast
 
-lemma qsum_subset_iff: "A <+> B \<subseteq> C <+> D <-> A<=C & B<=D"
+lemma qsum_subset_iff: "A <+> B \<subseteq> C <+> D \<longleftrightarrow> A<=C & B<=D"
 by blast
 
-lemma qsum_equal_iff: "A <+> B = C <+> D <-> A=C & B=D"
+lemma qsum_equal_iff: "A <+> B = C <+> D \<longleftrightarrow> A=C & B=D"
 apply (simp (no_asm) add: extension qsum_subset_iff)
 apply blast
 done
diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/QUniv.thy
--- a/src/ZF/QUniv.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/QUniv.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -130,7 +130,7 @@
 
 lemmas quniv_QPair_E = quniv_QPair_D [THEN conjE]
 
-lemma quniv_QPair_iff: "<a;b> \<in> quniv(A) <-> a: quniv(A) & b: quniv(A)"
+lemma quniv_QPair_iff: "<a;b> \<in> quniv(A) \<longleftrightarrow> a: quniv(A) & b: quniv(A)"
 by (blast intro: QPair_in_quniv dest: quniv_QPair_D)
 
 
diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/Sum.thy
--- a/src/ZF/Sum.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Sum.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -28,7 +28,7 @@
 subsection{*Rules for the @{term Part} Primitive*}
 
 lemma Part_iff: 
-    "a \<in> Part(A,h) <-> a:A & (\<exists>y. a=h(y))"
+    "a \<in> Part(A,h) \<longleftrightarrow> a:A & (\<exists>y. a=h(y))"
 apply (unfold Part_def)
 apply (rule separation)
 done
@@ -77,16 +77,16 @@
 
 (** Injection and freeness equivalences, for rewriting **)
 
-lemma Inl_iff [iff]: "Inl(a)=Inl(b) <-> a=b"
+lemma Inl_iff [iff]: "Inl(a)=Inl(b) \<longleftrightarrow> a=b"
 by (simp add: sum_defs)
 
-lemma Inr_iff [iff]: "Inr(a)=Inr(b) <-> a=b"
+lemma Inr_iff [iff]: "Inr(a)=Inr(b) \<longleftrightarrow> a=b"
 by (simp add: sum_defs)
 
-lemma Inl_Inr_iff [simp]: "Inl(a)=Inr(b) <-> False"
+lemma Inl_Inr_iff [simp]: "Inl(a)=Inr(b) \<longleftrightarrow> False"
 by (simp add: sum_defs)
 
-lemma Inr_Inl_iff [simp]: "Inr(b)=Inl(a) <-> False"
+lemma Inr_Inl_iff [simp]: "Inr(b)=Inl(a) \<longleftrightarrow> False"
 by (simp add: sum_defs)
 
 lemma sum_empty [simp]: "0+0 = 0"
@@ -106,19 +106,19 @@
 lemma InrD: "Inr(b): A+B ==> b: B"
 by blast
 
-lemma sum_iff: "u: A+B <-> (\<exists>x. x:A & u=Inl(x)) | (\<exists>y. y:B & u=Inr(y))"
+lemma sum_iff: "u: A+B \<longleftrightarrow> (\<exists>x. x:A & u=Inl(x)) | (\<exists>y. y:B & u=Inr(y))"
 by blast
 
-lemma Inl_in_sum_iff [simp]: "(Inl(x) \<in> A+B) <-> (x \<in> A)";
+lemma Inl_in_sum_iff [simp]: "(Inl(x) \<in> A+B) \<longleftrightarrow> (x \<in> A)";
 by auto
 
-lemma Inr_in_sum_iff [simp]: "(Inr(y) \<in> A+B) <-> (y \<in> B)";
+lemma Inr_in_sum_iff [simp]: "(Inr(y) \<in> A+B) \<longleftrightarrow> (y \<in> B)";
 by auto
 
-lemma sum_subset_iff: "A+B \<subseteq> C+D <-> A<=C & B<=D"
+lemma sum_subset_iff: "A+B \<subseteq> C+D \<longleftrightarrow> A<=C & B<=D"
 by blast
 
-lemma sum_equal_iff: "A+B = C+D <-> A=C & B=D"
+lemma sum_equal_iff: "A+B = C+D \<longleftrightarrow> A=C & B=D"
 by (simp add: extension sum_subset_iff, blast)
 
 lemma sum_eq_2_times: "A+A = 2*A"
@@ -141,7 +141,7 @@
 by auto
 
 lemma expand_case: "u: A+B ==>    
-        R(case(c,d,u)) <->  
+        R(case(c,d,u)) \<longleftrightarrow>  
         ((\<forall>x\<in>A. u = Inl(x) \<longrightarrow> R(c(x))) &  
         (\<forall>y\<in>B. u = Inr(y) \<longrightarrow> R(d(y))))"
 by auto
diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/Univ.thy
--- a/src/ZF/Univ.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/Univ.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -433,10 +433,10 @@
 by (blast intro: VsetI_lemma elim: ltE)
 
 text{*Merely a lemma for the next result*}
-lemma Vset_Ord_rank_iff: "Ord(i) ==> b \<in> Vset(i) <-> rank(b) < i"
+lemma Vset_Ord_rank_iff: "Ord(i) ==> b \<in> Vset(i) \<longleftrightarrow> rank(b) < i"
 by (blast intro: VsetD VsetI)
 
-lemma Vset_rank_iff [simp]: "b \<in> Vset(a) <-> rank(b) < rank(a)"
+lemma Vset_rank_iff [simp]: "b \<in> Vset(a) \<longleftrightarrow> rank(b) < rank(a)"
 apply (rule Vfrom_rank_eq [THEN subst])
 apply (rule Ord_rank [THEN Vset_Ord_rank_iff])
 done
@@ -766,10 +766,10 @@
 text{*This weaker version says a, b exist at the same level*}
 lemmas Vfrom_doubleton_D = Transset_Vfrom [THEN Transset_doubleton_D]
 
-(** Using only the weaker theorem would prove <a,b> : Vfrom(X,i)
-      implies a, b : Vfrom(X,i), which is useless for induction.
-    Using only the stronger theorem would prove <a,b> : Vfrom(X,succ(succ(i)))
-      implies a, b : Vfrom(X,i), leaving the succ(i) case untreated.
+(** Using only the weaker theorem would prove <a,b> \<in> Vfrom(X,i)
+      implies a, b \<in> Vfrom(X,i), which is useless for induction.
+    Using only the stronger theorem would prove <a,b> \<in> Vfrom(X,succ(succ(i)))
+      implies a, b \<in> Vfrom(X,i), leaving the succ(i) case untreated.
     The combination gives a reduction by precisely one level, which is
       most convenient for proofs.
 **)
diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/WF.thy
--- a/src/ZF/WF.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/WF.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -63,7 +63,7 @@
 lemma wf_on_field_imp_wf: "wf[field(r)](r) ==> wf(r)"
 by (unfold wf_def wf_on_def, fast)
 
-lemma wf_iff_wf_on_field: "wf(r) <-> wf[field(r)](r)"
+lemma wf_iff_wf_on_field: "wf(r) \<longleftrightarrow> wf[field(r)](r)"
 by (blast intro: wf_imp_wf_on wf_on_field_imp_wf)
 
 lemma wf_on_subset_A: "[| wf[A](r);  B<=A |] ==> wf[B](r)"
@@ -245,7 +245,7 @@
 apply (elim ssubst)
 apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def)
 apply (rule_tac t = "%z. H (?x,z) " in subst_context)
-apply (subgoal_tac "\<forall>y\<in>r-``{x}. \<forall>z. <y,z>:f <-> <y,z>:g")
+apply (subgoal_tac "\<forall>y\<in>r-``{x}. \<forall>z. <y,z>:f \<longleftrightarrow> <y,z>:g")
  apply (blast dest: transD)
 apply (simp add: apply_iff)
 apply (blast dest: transD intro: sym)
@@ -364,7 +364,7 @@
 
 text{*Minimal-element characterization of well-foundedness*}
 lemma wf_eq_minimal:
-     "wf(r) <-> (\<forall>Q x. x:Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. <y,z>:r \<longrightarrow> y\<notin>Q))"
+     "wf(r) \<longleftrightarrow> (\<forall>Q x. x:Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. <y,z>:r \<longrightarrow> y\<notin>Q))"
 by (unfold wf_def, blast)
 
 end
diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/equalities.thy
--- a/src/ZF/equalities.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/equalities.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -22,21 +22,21 @@
   The following are not added to the default simpset because
   (a) they duplicate the body and (b) there are no similar rules for @{text Int}.*}
 
-lemma ball_Un: "(\<forall>x \<in> A\<union>B. P(x)) <-> (\<forall>x \<in> A. P(x)) & (\<forall>x \<in> B. P(x))";
+lemma ball_Un: "(\<forall>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<forall>x \<in> A. P(x)) & (\<forall>x \<in> B. P(x))";
   by blast
 
-lemma bex_Un: "(\<exists>x \<in> A\<union>B. P(x)) <-> (\<exists>x \<in> A. P(x)) | (\<exists>x \<in> B. P(x))";
+lemma bex_Un: "(\<exists>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<exists>x \<in> A. P(x)) | (\<exists>x \<in> B. P(x))";
   by blast
 
-lemma ball_UN: "(\<forall>z \<in> (\<Union>x\<in>A. B(x)). P(z)) <-> (\<forall>x\<in>A. \<forall>z \<in> B(x). P(z))"
+lemma ball_UN: "(\<forall>z \<in> (\<Union>x\<in>A. B(x)). P(z)) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>z \<in> B(x). P(z))"
   by blast
 
-lemma bex_UN: "(\<exists>z \<in> (\<Union>x\<in>A. B(x)). P(z)) <-> (\<exists>x\<in>A. \<exists>z\<in>B(x). P(z))"
+lemma bex_UN: "(\<exists>z \<in> (\<Union>x\<in>A. B(x)). P(z)) \<longleftrightarrow> (\<exists>x\<in>A. \<exists>z\<in>B(x). P(z))"
   by blast
 
 subsection{*Converse of a Relation*}
 
-lemma converse_iff [simp]: "<a,b>\<in> converse(r) <-> <b,a>\<in>r"
+lemma converse_iff [simp]: "<a,b>\<in> converse(r) \<longleftrightarrow> <b,a>\<in>r"
 by (unfold converse_def, blast)
 
 lemma converseI [intro!]: "<a,b>\<in>r ==> <b,a>\<in>converse(r)"
@@ -64,7 +64,7 @@
 by blast
 
 lemma converse_subset_iff:
-     "A \<subseteq> Sigma(X,Y) ==> converse(A) \<subseteq> converse(B) <-> A \<subseteq> B"
+     "A \<subseteq> Sigma(X,Y) ==> converse(A) \<subseteq> converse(B) \<longleftrightarrow> A \<subseteq> B"
 by blast
 
 
@@ -76,17 +76,17 @@
 lemma subset_consI: "B \<subseteq> cons(a,B)"
 by blast
 
-lemma cons_subset_iff [iff]: "cons(a,B)\<subseteq>C <-> a\<in>C & B\<subseteq>C"
+lemma cons_subset_iff [iff]: "cons(a,B)\<subseteq>C \<longleftrightarrow> a\<in>C & B\<subseteq>C"
 by blast
 
 (*A safe special case of subset elimination, adding no new variables
   [| cons(a,B) \<subseteq> C; [| a \<in> C; B \<subseteq> C |] ==> R |] ==> R *)
 lemmas cons_subsetE = cons_subset_iff [THEN iffD1, THEN conjE]
 
-lemma subset_empty_iff: "A\<subseteq>0 <-> A=0"
+lemma subset_empty_iff: "A\<subseteq>0 \<longleftrightarrow> A=0"
 by blast
 
-lemma subset_cons_iff: "C\<subseteq>cons(a,B) <-> C\<subseteq>B | (a\<in>C & C-{a} \<subseteq> B)"
+lemma subset_cons_iff: "C\<subseteq>cons(a,B) \<longleftrightarrow> C\<subseteq>B | (a\<in>C & C-{a} \<subseteq> B)"
 by blast
 
 (* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*)
@@ -134,7 +134,7 @@
     "[| succ(i) \<subseteq> j;  [| i\<in>j;  i\<subseteq>j |] ==> P |] ==> P"
 by (unfold succ_def, blast)
 
-lemma succ_subset_iff: "succ(a) \<subseteq> B <-> (a \<subseteq> B & a \<in> B)"
+lemma succ_subset_iff: "succ(a) \<subseteq> B \<longleftrightarrow> (a \<subseteq> B & a \<in> B)"
 by (unfold succ_def, blast)
 
 
@@ -142,7 +142,7 @@
 
 (** Intersection is the greatest lower bound of two sets **)
 
-lemma Int_subset_iff: "C \<subseteq> A \<inter> B <-> C \<subseteq> A & C \<subseteq> B"
+lemma Int_subset_iff: "C \<subseteq> A \<inter> B \<longleftrightarrow> C \<subseteq> A & C \<subseteq> B"
 by blast
 
 lemma Int_lower1: "A \<inter> B \<subseteq> A"
@@ -187,10 +187,10 @@
 lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)"
 by blast
 
-lemma subset_Int_iff: "A\<subseteq>B <-> A \<inter> B = A"
+lemma subset_Int_iff: "A\<subseteq>B \<longleftrightarrow> A \<inter> B = A"
 by (blast elim!: equalityE)
 
-lemma subset_Int_iff2: "A\<subseteq>B <-> B \<inter> A = A"
+lemma subset_Int_iff2: "A\<subseteq>B \<longleftrightarrow> B \<inter> A = A"
 by (blast elim!: equalityE)
 
 lemma Int_Diff_eq: "C\<subseteq>A ==> (A-B) \<inter> C = C-B"
@@ -211,7 +211,7 @@
 
 (** Union is the least upper bound of two sets *)
 
-lemma Un_subset_iff: "A \<union> B \<subseteq> C <-> A \<subseteq> C & B \<subseteq> C"
+lemma Un_subset_iff: "A \<union> B \<subseteq> C \<longleftrightarrow> A \<subseteq> C & B \<subseteq> C"
 by blast
 
 lemma Un_upper1: "A \<subseteq> A \<union> B"
@@ -253,13 +253,13 @@
 lemma Un_Int_distrib: "(A \<inter> B) \<union> C  =  (A \<union> C) \<inter> (B \<union> C)"
 by blast
 
-lemma subset_Un_iff: "A\<subseteq>B <-> A \<union> B = B"
+lemma subset_Un_iff: "A\<subseteq>B \<longleftrightarrow> A \<union> B = B"
 by (blast elim!: equalityE)
 
-lemma subset_Un_iff2: "A\<subseteq>B <-> B \<union> A = B"
+lemma subset_Un_iff2: "A\<subseteq>B \<longleftrightarrow> B \<union> A = B"
 by (blast elim!: equalityE)
 
-lemma Un_empty [iff]: "(A \<union> B = 0) <-> (A = 0 & B = 0)"
+lemma Un_empty [iff]: "(A \<union> B = 0) \<longleftrightarrow> (A = 0 & B = 0)"
 by blast
 
 lemma Un_eq_Union: "A \<union> B = \<Union>({A, B})"
@@ -273,7 +273,7 @@
 lemma Diff_contains: "[| C\<subseteq>A;  C \<inter> B = 0 |] ==> C \<subseteq> A-B"
 by blast
 
-lemma subset_Diff_cons_iff: "B \<subseteq> A - cons(c,C)  <->  B\<subseteq>A-C & c \<notin> B"
+lemma subset_Diff_cons_iff: "B \<subseteq> A - cons(c,C)  \<longleftrightarrow>  B\<subseteq>A-C & c \<notin> B"
 by blast
 
 lemma Diff_cancel: "A - A = 0"
@@ -288,7 +288,7 @@
 lemma Diff_0 [simp]: "A - 0 = A"
 by blast
 
-lemma Diff_eq_0_iff: "A - B = 0 <-> A \<subseteq> B"
+lemma Diff_eq_0_iff: "A - B = 0 \<longleftrightarrow> A \<subseteq> B"
 by (blast elim: equalityE)
 
 (*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
@@ -338,7 +338,7 @@
 by blast
 
 (*Halmos, Naive Set Theory, page 16.*)
-lemma Un_Int_assoc_iff: "(A \<inter> B) \<union> C = A \<inter> (B \<union> C)  <->  C\<subseteq>A"
+lemma Un_Int_assoc_iff: "(A \<inter> B) \<union> C = A \<inter> (B \<union> C)  \<longleftrightarrow>  C\<subseteq>A"
 by (blast elim!: equalityE)
 
 
@@ -346,7 +346,7 @@
 
 (** Big Union is the least upper bound of a set  **)
 
-lemma Union_subset_iff: "\<Union>(A) \<subseteq> C <-> (\<forall>x\<in>A. x \<subseteq> C)"
+lemma Union_subset_iff: "\<Union>(A) \<subseteq> C \<longleftrightarrow> (\<forall>x\<in>A. x \<subseteq> C)"
 by blast
 
 lemma Union_upper: "B\<in>A ==> B \<subseteq> \<Union>(A)"
@@ -364,10 +364,10 @@
 lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>(A) \<inter> \<Union>(B)"
 by blast
 
-lemma Union_disjoint: "\<Union>(C) \<inter> A = 0 <-> (\<forall>B\<in>C. B \<inter> A = 0)"
+lemma Union_disjoint: "\<Union>(C) \<inter> A = 0 \<longleftrightarrow> (\<forall>B\<in>C. B \<inter> A = 0)"
 by (blast elim!: equalityE)
 
-lemma Union_empty_iff: "\<Union>(A) = 0 <-> (\<forall>B\<in>A. B=0)"
+lemma Union_empty_iff: "\<Union>(A) = 0 \<longleftrightarrow> (\<forall>B\<in>A. B=0)"
 by blast
 
 lemma Int_Union2: "\<Union>(B) \<inter> A = (\<Union>C\<in>B. C \<inter> A)"
@@ -375,7 +375,7 @@
 
 (** Big Intersection is the greatest lower bound of a nonempty set **)
 
-lemma Inter_subset_iff: "A\<noteq>0  ==>  C \<subseteq> \<Inter>(A) <-> (\<forall>x\<in>A. C \<subseteq> x)"
+lemma Inter_subset_iff: "A\<noteq>0  ==>  C \<subseteq> \<Inter>(A) \<longleftrightarrow> (\<forall>x\<in>A. C \<subseteq> x)"
 by blast
 
 lemma Inter_lower: "B\<in>A ==> \<Inter>(A) \<subseteq> B"
@@ -416,10 +416,10 @@
 
 subsection{*Unions and Intersections of Families*}
 
-lemma subset_UN_iff_eq: "A \<subseteq> (\<Union>i\<in>I. B(i)) <-> A = (\<Union>i\<in>I. A \<inter> B(i))"
+lemma subset_UN_iff_eq: "A \<subseteq> (\<Union>i\<in>I. B(i)) \<longleftrightarrow> A = (\<Union>i\<in>I. A \<inter> B(i))"
 by (blast elim!: equalityE)
 
-lemma UN_subset_iff: "(\<Union>x\<in>A. B(x)) \<subseteq> C <-> (\<forall>x\<in>A. B(x) \<subseteq> C)"
+lemma UN_subset_iff: "(\<Union>x\<in>A. B(x)) \<subseteq> C \<longleftrightarrow> (\<forall>x\<in>A. B(x) \<subseteq> C)"
 by blast
 
 lemma UN_upper: "x\<in>A ==> B(x) \<subseteq> (\<Union>x\<in>A. B(x))"
@@ -571,7 +571,7 @@
 by blast
 
 lemma times_subset_iff:
-     "(A'*B' \<subseteq> A*B) <-> (A' = 0 | B' = 0 | (A'\<subseteq>A) & (B'\<subseteq>B))"
+     "(A'*B' \<subseteq> A*B) \<longleftrightarrow> (A' = 0 | B' = 0 | (A'\<subseteq>A) & (B'\<subseteq>B))"
 by blast
 
 lemma Int_Sigma_eq:
@@ -580,7 +580,7 @@
 
 (** Domain **)
 
-lemma domain_iff: "a: domain(r) <-> (\<exists>y. <a,y>\<in> r)"
+lemma domain_iff: "a: domain(r) \<longleftrightarrow> (\<exists>y. <a,y>\<in> r)"
 by (unfold domain_def, blast)
 
 lemma domainI [intro]: "<a,b>\<in> r ==> a: domain(r)"
@@ -739,10 +739,10 @@
 
 subsection{*Image of a Set under a Function or Relation*}
 
-lemma image_iff: "b \<in> r``A <-> (\<exists>x\<in>A. <x,b>\<in>r)"
+lemma image_iff: "b \<in> r``A \<longleftrightarrow> (\<exists>x\<in>A. <x,b>\<in>r)"
 by (unfold image_def, blast)
 
-lemma image_singleton_iff: "b \<in> r``{a} <-> <a,b>\<in>r"
+lemma image_singleton_iff: "b \<in> r``{a} \<longleftrightarrow> <a,b>\<in>r"
 by (rule image_iff [THEN iff_trans], blast)
 
 lemma imageI [intro]: "[| <a,b>\<in> r;  a\<in>A |] ==> b \<in> r``A"
@@ -792,10 +792,10 @@
 subsection{*Inverse Image of a Set under a Function or Relation*}
 
 lemma vimage_iff:
-    "a \<in> r-``B <-> (\<exists>y\<in>B. <a,y>\<in>r)"
+    "a \<in> r-``B \<longleftrightarrow> (\<exists>y\<in>B. <a,y>\<in>r)"
 by (unfold vimage_def image_def converse_def, blast)
 
-lemma vimage_singleton_iff: "a \<in> r-``{b} <-> <a,b>\<in>r"
+lemma vimage_singleton_iff: "a \<in> r-``{b} \<longleftrightarrow> <a,b>\<in>r"
 by (rule vimage_iff [THEN iff_trans], blast)
 
 lemma vimageI [intro]: "[| <a,b>\<in> r;  b\<in>B |] ==> a \<in> r-``B"
@@ -897,7 +897,7 @@
 lemma Union_Pow_eq [simp]: "\<Union>(Pow(A)) = A"
 by blast
 
-lemma Union_Pow_iff: "\<Union>(A) \<in> Pow(B) <-> A \<in> Pow(Pow(B))"
+lemma Union_Pow_iff: "\<Union>(A) \<in> Pow(B) \<longleftrightarrow> A \<in> Pow(Pow(B))"
 by blast
 
 lemma Pow_Int_eq [simp]: "Pow(A \<inter> B) = Pow(A) \<inter> Pow(B)"
@@ -912,7 +912,7 @@
 lemma RepFun_subset: "[| !!x. x\<in>A ==> f(x) \<in> B |] ==> {f(x). x\<in>A} \<subseteq> B"
 by blast
 
-lemma RepFun_eq_0_iff [simp]: "{f(x).x\<in>A}=0 <-> A=0"
+lemma RepFun_eq_0_iff [simp]: "{f(x).x\<in>A}=0 \<longleftrightarrow> A=0"
 by blast
 
 lemma RepFun_constant [simp]: "{c. x\<in>A} = (if A=0 then 0 else {c})"
diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/ex/Ring.thy
--- a/src/ZF/ex/Ring.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/ex/Ring.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -6,6 +6,10 @@
 
 theory Ring imports Group begin
 
+no_notation
+  cadd  (infixl "\<oplus>" 65) and
+  cmult  (infixl "\<otimes>" 70)
+
 (*First, we must simulate a record declaration:
 record ring = monoid +
   add :: "[i, i] => i" (infixl "\<oplus>\<index>" 65)
@@ -46,7 +50,7 @@
   "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus>\<^bsub>R\<^esub> y = x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
 
 locale abelian_monoid = fixes G (structure)
-  assumes a_comm_monoid: 
+  assumes a_comm_monoid:
     "comm_monoid (<carrier(G), add_field(G), zero(G), 0>)"
 
 text {*
@@ -54,7 +58,7 @@
 *}
 
 locale abelian_group = abelian_monoid +
-  assumes a_comm_group: 
+  assumes a_comm_group:
     "comm_group (<carrier(G), add_field(G), zero(G), 0>)"
 
 locale ring = abelian_group R + monoid R for R (structure) +
@@ -75,21 +79,21 @@
 
 lemma (in abelian_monoid) a_monoid:
      "monoid (<carrier(G), add_field(G), zero(G), 0>)"
-apply (insert a_comm_monoid) 
-apply (simp add: comm_monoid_def) 
+apply (insert a_comm_monoid)
+apply (simp add: comm_monoid_def)
 done
 
 lemma (in abelian_group) a_group:
      "group (<carrier(G), add_field(G), zero(G), 0>)"
-apply (insert a_comm_group) 
-apply (simp add: comm_group_def group_def) 
+apply (insert a_comm_group)
+apply (simp add: comm_group_def group_def)
 done
 
 
 lemma (in abelian_monoid) l_zero [simp]:
      "x \<in> carrier(G) \<Longrightarrow> \<zero> \<oplus> x = x"
 apply (insert monoid.l_one [OF a_monoid])
-apply (simp add: ring_add_def) 
+apply (simp add: ring_add_def)
 done
 
 lemma (in abelian_monoid) zero_closed [intro, simp]:
@@ -102,7 +106,7 @@
 
 lemma (in abelian_monoid) a_closed [intro, simp]:
      "[| x \<in> carrier(G); y \<in> carrier(G) |] ==> x \<oplus> y \<in> carrier(G)"
-by (rule monoid.m_closed [OF a_monoid, 
+by (rule monoid.m_closed [OF a_monoid,
                   simplified, simplified ring_add_def [symmetric]])
 
 lemma (in abelian_group) minus_closed [intro, simp]:
@@ -110,18 +114,18 @@
 by (simp add: minus_def)
 
 lemma (in abelian_group) a_l_cancel [simp]:
-     "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> 
+     "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
       \<Longrightarrow> (x \<oplus> y = x \<oplus> z) <-> (y = z)"
-by (rule group.l_cancel [OF a_group, 
+by (rule group.l_cancel [OF a_group,
              simplified, simplified ring_add_def [symmetric]])
 
 lemma (in abelian_group) a_r_cancel [simp]:
-     "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> 
+     "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
       \<Longrightarrow> (y \<oplus> x = z \<oplus> x) <-> (y = z)"
 by (rule group.r_cancel [OF a_group, simplified, simplified ring_add_def [symmetric]])
 
 lemma (in abelian_monoid) a_assoc:
-  "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> 
+  "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
    \<Longrightarrow> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
 by (rule monoid.m_assoc [OF a_monoid, simplified, simplified ring_add_def [symmetric]])
 
@@ -136,7 +140,7 @@
     simplified, simplified ring_add_def [symmetric]])
 
 lemma (in abelian_monoid) a_lcomm:
-     "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> 
+     "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
       \<Longrightarrow> x \<oplus> (y \<oplus> z) = y \<oplus> (x \<oplus> z)"
 by (rule comm_monoid.m_lcomm [OF a_comm_monoid,
     simplified, simplified ring_add_def [symmetric]])
@@ -168,7 +172,7 @@
 
 lemmas (in abelian_monoid) a_ac = a_assoc a_comm a_lcomm
 
-text {* 
+text {*
   The following proofs are from Jacobson, Basic Algebra I, pp.~88--89
 *}
 
@@ -179,7 +183,7 @@
 proof -
   assume R: "x \<in> carrier(R)"
   then have "\<zero> \<cdot> x \<oplus> \<zero> \<cdot> x = (\<zero> \<oplus> \<zero>) \<cdot> x"
-    by (blast intro: l_distr [THEN sym]) 
+    by (blast intro: l_distr [THEN sym])
   also from R have "... = \<zero> \<cdot> x \<oplus> \<zero>" by simp
   finally have "\<zero> \<cdot> x \<oplus> \<zero> \<cdot> x = \<zero> \<cdot> x \<oplus> \<zero>" .
   with R show ?thesis by (simp del: r_zero)
@@ -250,12 +254,12 @@
 by (auto simp add: ring_hom_def)
 
 lemma ring_hom_mult:
-     "\<lbrakk>h \<in> ring_hom(R,S); x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> 
+     "\<lbrakk>h \<in> ring_hom(R,S); x \<in> carrier(R); y \<in> carrier(R)\<rbrakk>
       \<Longrightarrow> h ` (x \<cdot>\<^bsub>R\<^esub> y) = (h ` x) \<cdot>\<^bsub>S\<^esub> (h ` y)"
 by (simp add: ring_hom_def)
 
 lemma ring_hom_add:
-     "\<lbrakk>h \<in> ring_hom(R,S); x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> 
+     "\<lbrakk>h \<in> ring_hom(R,S); x \<in> carrier(R); y \<in> carrier(R)\<rbrakk>
       \<Longrightarrow> h ` (x \<oplus>\<^bsub>R\<^esub> y) = (h ` x) \<oplus>\<^bsub>S\<^esub> (h ` y)"
 by (simp add: ring_hom_def)
 
@@ -288,8 +292,8 @@
 qed
 
 lemma (in ring) id_ring_hom [simp]: "id(carrier(R)) \<in> ring_hom(R,R)"
-apply (rule ring_hom_memI)  
-apply (auto simp add: id_type) 
+apply (rule ring_hom_memI)
+apply (auto simp add: id_type)
 done
 
 end
diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/func.thy
--- a/src/ZF/func.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/func.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -20,12 +20,12 @@
 by (simp add: restrict_def relation_def, blast) 
 
 lemma Pi_iff:
-    "f: Pi(A,B) <-> function(f) & f<=Sigma(A,B) & A<=domain(f)"
+    "f: Pi(A,B) \<longleftrightarrow> function(f) & f<=Sigma(A,B) & A<=domain(f)"
 by (unfold Pi_def, blast)
 
 (*For upward compatibility with the former definition*)
 lemma Pi_iff_old:
-    "f: Pi(A,B) <-> f<=Sigma(A,B) & (\<forall>x\<in>A. EX! y. <x,y>: f)"
+    "f: Pi(A,B) \<longleftrightarrow> f<=Sigma(A,B) & (\<forall>x\<in>A. EX! y. <x,y>: f)"
 by (unfold Pi_def function_def, blast)
 
 lemma fun_is_function: "f: Pi(A,B) ==> function(f)"
@@ -96,7 +96,7 @@
 lemma apply_funtype: "[| f: A->B;  a:A |] ==> f`a \<in> B"
 by (blast dest: apply_type)
 
-lemma apply_iff: "f: Pi(A,B) ==> <a,b>: f <-> a:A & f`a = b"
+lemma apply_iff: "f: Pi(A,B) ==> <a,b>: f \<longleftrightarrow> a:A & f`a = b"
 apply (frule fun_is_rel)
 apply (blast intro!: apply_Pair apply_equality)
 done
@@ -110,7 +110,7 @@
 (*Such functions arise in non-standard datatypes, ZF/ex/Ntree for instance*)
 lemma Pi_Collect_iff:
      "(f \<in> Pi(A, %x. {y:B(x). P(x,y)}))
-      <->  f \<in> Pi(A,B) & (\<forall>x\<in>A. P(x, f`x))"
+      \<longleftrightarrow>  f \<in> Pi(A,B) & (\<forall>x\<in>A. P(x, f`x))"
 by (blast intro: Pi_type dest: apply_type)
 
 lemma Pi_weaken_type:
@@ -222,11 +222,11 @@
 done
 
 lemma fun_extension_iff:
-     "[| f:Pi(A,B); g:Pi(A,C) |] ==> (\<forall>a\<in>A. f`a = g`a) <-> f=g"
+     "[| f:Pi(A,B); g:Pi(A,C) |] ==> (\<forall>a\<in>A. f`a = g`a) \<longleftrightarrow> f=g"
 by (blast intro: fun_extension)
 
 (*thm by Mark Staples, proof by lcp*)
-lemma fun_subset_eq: "[| f:Pi(A,B); g:Pi(A,C) |] ==> f \<subseteq> g <-> (f = g)"
+lemma fun_subset_eq: "[| f:Pi(A,B); g:Pi(A,C) |] ==> f \<subseteq> g \<longleftrightarrow> (f = g)"
 by (blast dest: apply_Pair
           intro: fun_extension apply_equality [symmetric])
 
@@ -592,7 +592,7 @@
 (* Useful with simp; contributed by Clemens Ballarin. *)
 
 lemma bex_image_simp:
-  "[| f \<in> Pi(X, Y); A \<subseteq> X |]  ==> (\<exists>x\<in>f``A. P(x)) <-> (\<exists>x\<in>A. P(f`x))"
+  "[| f \<in> Pi(X, Y); A \<subseteq> X |]  ==> (\<exists>x\<in>f``A. P(x)) \<longleftrightarrow> (\<exists>x\<in>A. P(f`x))"
   apply safe
    apply rule
     prefer 2 apply assumption
@@ -601,7 +601,7 @@
   done
 
 lemma ball_image_simp:
-  "[| f \<in> Pi(X, Y); A \<subseteq> X |]  ==> (\<forall>x\<in>f``A. P(x)) <-> (\<forall>x\<in>A. P(f`x))"
+  "[| f \<in> Pi(X, Y); A \<subseteq> X |]  ==> (\<forall>x\<in>f``A. P(x)) \<longleftrightarrow> (\<forall>x\<in>A. P(f`x))"
   apply safe
    apply (blast intro: apply_Pair)
   apply (drule bspec) apply assumption
diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/pair.thy
--- a/src/ZF/pair.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/pair.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -34,13 +34,13 @@
 
 (** Lemmas for showing that <a,b> uniquely determines a and b **)
 
-lemma singleton_eq_iff [iff]: "{a} = {b} <-> a=b"
+lemma singleton_eq_iff [iff]: "{a} = {b} \<longleftrightarrow> a=b"
 by (rule extension [THEN iff_trans], blast)
 
-lemma doubleton_eq_iff: "{a,b} = {c,d} <-> (a=c & b=d) | (a=d & b=c)"
+lemma doubleton_eq_iff: "{a,b} = {c,d} \<longleftrightarrow> (a=c & b=d) | (a=d & b=c)"
 by (rule extension [THEN iff_trans], blast)
 
-lemma Pair_iff [simp]: "<a,b> = <c,d> <-> a=c & b=d"
+lemma Pair_iff [simp]: "<a,b> = <c,d> \<longleftrightarrow> a=c & b=d"
 by (simp add: Pair_def doubleton_eq_iff, blast)
 
 lemmas Pair_inject = Pair_iff [THEN iffD1, THEN conjE, elim!]
@@ -76,7 +76,7 @@
 
 text{*Generalizes Cartesian product*}
 
-lemma Sigma_iff [simp]: "<a,b>: Sigma(A,B) <-> a:A & b:B(a)"
+lemma Sigma_iff [simp]: "<a,b>: Sigma(A,B) \<longleftrightarrow> a:A & b:B(a)"
 by (simp add: Sigma_def)
 
 lemma SigmaI [TC,intro!]: "[| a:A;  b:B(a) |] ==> <a,b> \<in> Sigma(A,B)"
@@ -113,7 +113,7 @@
 lemma Sigma_empty2 [simp]: "A*0 = 0"
 by blast
 
-lemma Sigma_empty_iff: "A*B=0 <-> A=0 | B=0"
+lemma Sigma_empty_iff: "A*B=0 \<longleftrightarrow> A=0 | B=0"
 by blast
 
 
@@ -150,7 +150,7 @@
 
 lemma expand_split: 
   "u: A*B ==>    
-        R(split(c,u)) <-> (\<forall>x\<in>A. \<forall>y\<in>B. u = <x,y> \<longrightarrow> R(c(x,y)))"
+        R(split(c,u)) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. u = <x,y> \<longrightarrow> R(c(x,y)))"
 apply (simp add: split_def)
 apply auto
 done
@@ -177,11 +177,11 @@
 *}
 
 lemma split_paired_Bex_Sigma [simp]:
-     "(\<exists>z \<in> Sigma(A,B). P(z)) <-> (\<exists>x \<in> A. \<exists>y \<in> B(x). P(<x,y>))"
+     "(\<exists>z \<in> Sigma(A,B). P(z)) \<longleftrightarrow> (\<exists>x \<in> A. \<exists>y \<in> B(x). P(<x,y>))"
 by blast
 
 lemma split_paired_Ball_Sigma [simp]:
-     "(\<forall>z \<in> Sigma(A,B). P(z)) <-> (\<forall>x \<in> A. \<forall>y \<in> B(x). P(<x,y>))"
+     "(\<forall>z \<in> Sigma(A,B). P(z)) \<longleftrightarrow> (\<forall>x \<in> A. \<forall>y \<in> B(x). P(<x,y>))"
 by blast
 
 end
diff -r c656222c4dc1 -r ff6b0c1087f2 src/ZF/upair.thy
--- a/src/ZF/upair.thy	Tue Mar 06 15:15:49 2012 +0000
+++ b/src/ZF/upair.thy	Tue Mar 06 16:06:52 2012 +0000
@@ -23,7 +23,7 @@
 
 subsection{*Unordered Pairs: constant @{term Upair}*}
 
-lemma Upair_iff [simp]: "c \<in> Upair(a,b) <-> (c=a | c=b)"
+lemma Upair_iff [simp]: "c \<in> Upair(a,b) \<longleftrightarrow> (c=a | c=b)"
 by (unfold Upair_def, blast)
 
 lemma UpairI1: "a \<in> Upair(a,b)"
@@ -37,7 +37,7 @@
 
 subsection{*Rules for Binary Union, Defined via @{term Upair}*}
 
-lemma Un_iff [simp]: "c \<in> A \<union> B <-> (c:A | c:B)"
+lemma Un_iff [simp]: "c \<in> A \<union> B \<longleftrightarrow> (c:A | c:B)"
 apply (simp add: Un_def)
 apply (blast intro: UpairI1 UpairI2 elim: UpairE)
 done
@@ -63,7 +63,7 @@
 
 subsection{*Rules for Binary Intersection, Defined via @{term Upair}*}
 
-lemma Int_iff [simp]: "c \<in> A \<inter> B <-> (c:A & c:B)"
+lemma Int_iff [simp]: "c \<in> A \<inter> B \<longleftrightarrow> (c:A & c:B)"
 apply (unfold Int_def)
 apply (blast intro: UpairI1 UpairI2 elim: UpairE)
 done
@@ -83,7 +83,7 @@
 
 subsection{*Rules for Set Difference, Defined via @{term Upair}*}
 
-lemma Diff_iff [simp]: "c \<in> A-B <-> (c:A & c\<notin>B)"
+lemma Diff_iff [simp]: "c \<in> A-B \<longleftrightarrow> (c:A & c\<notin>B)"
 by (unfold Diff_def, blast)
 
 lemma DiffI [intro!]: "[| c \<in> A;  c \<notin> B |] ==> c \<in> A - B"
@@ -101,7 +101,7 @@
 
 subsection{*Rules for @{term cons}*}
 
-lemma cons_iff [simp]: "a \<in> cons(b,A) <-> (a=b | a:A)"
+lemma cons_iff [simp]: "a \<in> cons(b,A) \<longleftrightarrow> (a=b | a:A)"
 apply (unfold cons_def)
 apply (blast intro: UpairI1 UpairI2 elim: UpairE)
 done
@@ -137,7 +137,7 @@
 
 subsection{*Singletons*}
 
-lemma singleton_iff: "a \<in> {b} <-> a=b"
+lemma singleton_iff: "a \<in> {b} \<longleftrightarrow> a=b"
 by simp
 
 lemma singletonI [intro!]: "a \<in> {a}"
@@ -164,7 +164,7 @@
 apply (blast+)
 done
 
-(*No congruence rule is necessary: if @{term"\<forall>y.P(y)<->Q(y)"} then
+(*No congruence rule is necessary: if @{term"\<forall>y.P(y)\<longleftrightarrow>Q(y)"} then
   @{term "THE x.P(x)"}  rewrites to @{term "THE x.Q(x)"} *)
 
 (*If it's "undefined", it's zero!*)
@@ -203,13 +203,13 @@
 
 (*Never use with case splitting, or if P is known to be true or false*)
 lemma if_cong:
-    "[| P<->Q;  Q ==> a=c;  ~Q ==> b=d |]
+    "[| P\<longleftrightarrow>Q;  Q ==> a=c;  ~Q ==> b=d |]
      ==> (if P then a else b) = (if Q then c else d)"
 by (simp add: if_def cong add: conj_cong)
 
 (*Prevents simplification of x and y: faster and allows the execution
   of functional programs. NOW THE DEFAULT.*)
-lemma if_weak_cong: "P<->Q ==> (if P then x else y) = (if Q then x else y)"
+lemma if_weak_cong: "P\<longleftrightarrow>Q ==> (if P then x else y) = (if Q then x else y)"
 by simp
 
 (*Not needed for rewriting, since P would rewrite to True anyway*)
@@ -221,7 +221,7 @@
 by (unfold if_def, blast)
 
 lemma split_if [split]:
-     "P(if Q then x else y) <-> ((Q \<longrightarrow> P(x)) & (~Q \<longrightarrow> P(y)))"
+     "P(if Q then x else y) \<longleftrightarrow> ((Q \<longrightarrow> P(x)) & (~Q \<longrightarrow> P(y)))"
 by (case_tac Q, simp_all)
 
 (** Rewrite rules for boolean case-splitting: faster than split_if [split]
@@ -236,7 +236,7 @@
 lemmas split_ifs = split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2
 
 (*Logically equivalent to split_if_mem2*)
-lemma if_iff: "a: (if P then x else y) <-> P & a:x | ~P & a:y"
+lemma if_iff: "a: (if P then x else y) \<longleftrightarrow> P & a:x | ~P & a:y"
 by simp
 
 lemma if_type [TC]:
@@ -245,7 +245,7 @@
 
 (** Splitting IFs in the assumptions **)
 
-lemma split_if_asm: "P(if Q then x else y) <-> (~((Q & ~P(x)) | (~Q & ~P(y))))"
+lemma split_if_asm: "P(if Q then x else y) \<longleftrightarrow> (~((Q & ~P(x)) | (~Q & ~P(y))))"
 by simp
 
 lemmas if_splits = split_if split_if_asm
@@ -281,7 +281,7 @@
 
 subsection{*Rules for Successor*}
 
-lemma succ_iff: "i \<in> succ(j) <-> i=j | i:j"
+lemma succ_iff: "i \<in> succ(j) \<longleftrightarrow> i=j | i:j"
 by (unfold succ_def, blast)
 
 lemma succI1 [simp]: "i \<in> succ(i)"
@@ -313,7 +313,7 @@
 (* @{term"succ(b) \<noteq> b"} *)
 lemmas succ_neq_self = succI1 [THEN mem_imp_not_eq, THEN not_sym]
 
-lemma succ_inject_iff [simp]: "succ(m) = succ(n) <-> m=n"
+lemma succ_inject_iff [simp]: "succ(m) = succ(n) \<longleftrightarrow> m=n"
 by (blast elim: mem_asym elim!: equalityE)
 
 lemmas succ_inject = succ_inject_iff [THEN iffD1, dest!]
@@ -322,83 +322,83 @@
 subsection{*Miniscoping of the Bounded Universal Quantifier*}
 
 lemma ball_simps1:
-     "(\<forall>x\<in>A. P(x) & Q)   <-> (\<forall>x\<in>A. P(x)) & (A=0 | Q)"
-     "(\<forall>x\<in>A. P(x) | Q)   <-> ((\<forall>x\<in>A. P(x)) | Q)"
-     "(\<forall>x\<in>A. P(x) \<longrightarrow> Q) <-> ((\<exists>x\<in>A. P(x)) \<longrightarrow> Q)"
-     "(~(\<forall>x\<in>A. P(x))) <-> (\<exists>x\<in>A. ~P(x))"
-     "(\<forall>x\<in>0.P(x)) <-> True"
-     "(\<forall>x\<in>succ(i).P(x)) <-> P(i) & (\<forall>x\<in>i. P(x))"
-     "(\<forall>x\<in>cons(a,B).P(x)) <-> P(a) & (\<forall>x\<in>B. P(x))"
-     "(\<forall>x\<in>RepFun(A,f). P(x)) <-> (\<forall>y\<in>A. P(f(y)))"
-     "(\<forall>x\<in>\<Union>(A).P(x)) <-> (\<forall>y\<in>A. \<forall>x\<in>y. P(x))"
+     "(\<forall>x\<in>A. P(x) & Q)   \<longleftrightarrow> (\<forall>x\<in>A. P(x)) & (A=0 | Q)"
+     "(\<forall>x\<in>A. P(x) | Q)   \<longleftrightarrow> ((\<forall>x\<in>A. P(x)) | Q)"
+     "(\<forall>x\<in>A. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x\<in>A. P(x)) \<longrightarrow> Q)"
+     "(~(\<forall>x\<in>A. P(x))) \<longleftrightarrow> (\<exists>x\<in>A. ~P(x))"
+     "(\<forall>x\<in>0.P(x)) \<longleftrightarrow> True"
+     "(\<forall>x\<in>succ(i).P(x)) \<longleftrightarrow> P(i) & (\<forall>x\<in>i. P(x))"
+     "(\<forall>x\<in>cons(a,B).P(x)) \<longleftrightarrow> P(a) & (\<forall>x\<in>B. P(x))"
+     "(\<forall>x\<in>RepFun(A,f). P(x)) \<longleftrightarrow> (\<forall>y\<in>A. P(f(y)))"
+     "(\<forall>x\<in>\<Union>(A).P(x)) \<longleftrightarrow> (\<forall>y\<in>A. \<forall>x\<in>y. P(x))"
 by blast+
 
 lemma ball_simps2:
-     "(\<forall>x\<in>A. P & Q(x))   <-> (A=0 | P) & (\<forall>x\<in>A. Q(x))"
-     "(\<forall>x\<in>A. P | Q(x))   <-> (P | (\<forall>x\<in>A. Q(x)))"
-     "(\<forall>x\<in>A. P \<longrightarrow> Q(x)) <-> (P \<longrightarrow> (\<forall>x\<in>A. Q(x)))"
+     "(\<forall>x\<in>A. P & Q(x))   \<longleftrightarrow> (A=0 | P) & (\<forall>x\<in>A. Q(x))"
+     "(\<forall>x\<in>A. P | Q(x))   \<longleftrightarrow> (P | (\<forall>x\<in>A. Q(x)))"
+     "(\<forall>x\<in>A. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x\<in>A. Q(x)))"
 by blast+
 
 lemma ball_simps3:
-     "(\<forall>x\<in>Collect(A,Q).P(x)) <-> (\<forall>x\<in>A. Q(x) \<longrightarrow> P(x))"
+     "(\<forall>x\<in>Collect(A,Q).P(x)) \<longleftrightarrow> (\<forall>x\<in>A. Q(x) \<longrightarrow> P(x))"
 by blast+
 
 lemmas ball_simps [simp] = ball_simps1 ball_simps2 ball_simps3
 
 lemma ball_conj_distrib:
-    "(\<forall>x\<in>A. P(x) & Q(x)) <-> ((\<forall>x\<in>A. P(x)) & (\<forall>x\<in>A. Q(x)))"
+    "(\<forall>x\<in>A. P(x) & Q(x)) \<longleftrightarrow> ((\<forall>x\<in>A. P(x)) & (\<forall>x\<in>A. Q(x)))"
 by blast
 
 
 subsection{*Miniscoping of the Bounded Existential Quantifier*}
 
 lemma bex_simps1:
-     "(\<exists>x\<in>A. P(x) & Q) <-> ((\<exists>x\<in>A. P(x)) & Q)"
-     "(\<exists>x\<in>A. P(x) | Q) <-> (\<exists>x\<in>A. P(x)) | (A\<noteq>0 & Q)"
-     "(\<exists>x\<in>A. P(x) \<longrightarrow> Q) <-> ((\<forall>x\<in>A. P(x)) \<longrightarrow> (A\<noteq>0 & Q))"
-     "(\<exists>x\<in>0.P(x)) <-> False"
-     "(\<exists>x\<in>succ(i).P(x)) <-> P(i) | (\<exists>x\<in>i. P(x))"
-     "(\<exists>x\<in>cons(a,B).P(x)) <-> P(a) | (\<exists>x\<in>B. P(x))"
-     "(\<exists>x\<in>RepFun(A,f). P(x)) <-> (\<exists>y\<in>A. P(f(y)))"
-     "(\<exists>x\<in>\<Union>(A).P(x)) <-> (\<exists>y\<in>A. \<exists>x\<in>y.  P(x))"
-     "(~(\<exists>x\<in>A. P(x))) <-> (\<forall>x\<in>A. ~P(x))"
+     "(\<exists>x\<in>A. P(x) & Q) \<longleftrightarrow> ((\<exists>x\<in>A. P(x)) & Q)"
+     "(\<exists>x\<in>A. P(x) | Q) \<longleftrightarrow> (\<exists>x\<in>A. P(x)) | (A\<noteq>0 & Q)"
+     "(\<exists>x\<in>A. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<forall>x\<in>A. P(x)) \<longrightarrow> (A\<noteq>0 & Q))"
+     "(\<exists>x\<in>0.P(x)) \<longleftrightarrow> False"
+     "(\<exists>x\<in>succ(i).P(x)) \<longleftrightarrow> P(i) | (\<exists>x\<in>i. P(x))"
+     "(\<exists>x\<in>cons(a,B).P(x)) \<longleftrightarrow> P(a) | (\<exists>x\<in>B. P(x))"
+     "(\<exists>x\<in>RepFun(A,f). P(x)) \<longleftrightarrow> (\<exists>y\<in>A. P(f(y)))"
+     "(\<exists>x\<in>\<Union>(A).P(x)) \<longleftrightarrow> (\<exists>y\<in>A. \<exists>x\<in>y.  P(x))"
+     "(~(\<exists>x\<in>A. P(x))) \<longleftrightarrow> (\<forall>x\<in>A. ~P(x))"
 by blast+
 
 lemma bex_simps2:
-     "(\<exists>x\<in>A. P & Q(x)) <-> (P & (\<exists>x\<in>A. Q(x)))"
-     "(\<exists>x\<in>A. P | Q(x)) <-> (A\<noteq>0 & P) | (\<exists>x\<in>A. Q(x))"
-     "(\<exists>x\<in>A. P \<longrightarrow> Q(x)) <-> ((A=0 | P) \<longrightarrow> (\<exists>x\<in>A. Q(x)))"
+     "(\<exists>x\<in>A. P & Q(x)) \<longleftrightarrow> (P & (\<exists>x\<in>A. Q(x)))"
+     "(\<exists>x\<in>A. P | Q(x)) \<longleftrightarrow> (A\<noteq>0 & P) | (\<exists>x\<in>A. Q(x))"
+     "(\<exists>x\<in>A. P \<longrightarrow> Q(x)) \<longleftrightarrow> ((A=0 | P) \<longrightarrow> (\<exists>x\<in>A. Q(x)))"
 by blast+
 
 lemma bex_simps3:
-     "(\<exists>x\<in>Collect(A,Q).P(x)) <-> (\<exists>x\<in>A. Q(x) & P(x))"
+     "(\<exists>x\<in>Collect(A,Q).P(x)) \<longleftrightarrow> (\<exists>x\<in>A. Q(x) & P(x))"
 by blast
 
 lemmas bex_simps [simp] = bex_simps1 bex_simps2 bex_simps3
 
 lemma bex_disj_distrib:
-    "(\<exists>x\<in>A. P(x) | Q(x)) <-> ((\<exists>x\<in>A. P(x)) | (\<exists>x\<in>A. Q(x)))"
+    "(\<exists>x\<in>A. P(x) | Q(x)) \<longleftrightarrow> ((\<exists>x\<in>A. P(x)) | (\<exists>x\<in>A. Q(x)))"
 by blast
 
 
 (** One-point rule for bounded quantifiers: see HOL/Set.ML **)
 
-lemma bex_triv_one_point1 [simp]: "(\<exists>x\<in>A. x=a) <-> (a:A)"
+lemma bex_triv_one_point1 [simp]: "(\<exists>x\<in>A. x=a) \<longleftrightarrow> (a:A)"
 by blast
 
-lemma bex_triv_one_point2 [simp]: "(\<exists>x\<in>A. a=x) <-> (a:A)"
+lemma bex_triv_one_point2 [simp]: "(\<exists>x\<in>A. a=x) \<longleftrightarrow> (a:A)"
 by blast
 
-lemma bex_one_point1 [simp]: "(\<exists>x\<in>A. x=a & P(x)) <-> (a:A & P(a))"
+lemma bex_one_point1 [simp]: "(\<exists>x\<in>A. x=a & P(x)) \<longleftrightarrow> (a:A & P(a))"
 by blast
 
-lemma bex_one_point2 [simp]: "(\<exists>x\<in>A. a=x & P(x)) <-> (a:A & P(a))"
+lemma bex_one_point2 [simp]: "(\<exists>x\<in>A. a=x & P(x)) \<longleftrightarrow> (a:A & P(a))"
 by blast
 
-lemma ball_one_point1 [simp]: "(\<forall>x\<in>A. x=a \<longrightarrow> P(x)) <-> (a:A \<longrightarrow> P(a))"
+lemma ball_one_point1 [simp]: "(\<forall>x\<in>A. x=a \<longrightarrow> P(x)) \<longleftrightarrow> (a:A \<longrightarrow> P(a))"
 by blast
 
-lemma ball_one_point2 [simp]: "(\<forall>x\<in>A. a=x \<longrightarrow> P(x)) <-> (a:A \<longrightarrow> P(a))"
+lemma ball_one_point2 [simp]: "(\<forall>x\<in>A. a=x \<longrightarrow> P(x)) \<longleftrightarrow> (a:A \<longrightarrow> P(a))"
 by blast