# HG changeset patch
# User wenzelm
# Date 1451232981 -3600
# Node ID 31f2105521eeff2b58082bb7a5f8b31381e0fb2a
# Parent  97c06cfd31e59f8a4204cea05bdd6fc588ecbca0
discontinued ASCII replacement syntax <->;

diff -r 97c06cfd31e5 -r 31f2105521ee NEWS
--- a/NEWS	Sun Dec 27 16:40:09 2015 +0100
+++ b/NEWS	Sun Dec 27 17:16:21 2015 +0100
@@ -474,6 +474,8 @@
 The subsequent commands help to reproduce the old forms, e.g. to
 simplify porting old theories:
 
+  notation iff  (infixr "<->" 25)
+
   type_notation Map.map  (infixr "~=>" 0)
   notation Map.map_comp  (infixl "o'_m" 55)
 
diff -r 97c06cfd31e5 -r 31f2105521ee src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Sun Dec 27 16:40:09 2015 +0100
+++ b/src/HOL/Fields.thy	Sun Dec 27 17:16:21 2015 +0100
@@ -1116,7 +1116,7 @@
 by (auto simp add: divide_less_eq)
 
 lemma divide_less_eq_1_neg [simp]:
-  "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"
+  "a < 0 \<Longrightarrow> b/a < 1 \<longleftrightarrow> a < b"
 by (auto simp add: divide_less_eq)
 
 lemma eq_divide_eq_1 [simp]:
diff -r 97c06cfd31e5 -r 31f2105521ee src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sun Dec 27 16:40:09 2015 +0100
+++ b/src/HOL/HOL.thy	Sun Dec 27 17:16:21 2015 +0100
@@ -113,11 +113,8 @@
   not_equal  (infix "\<noteq>" 50)
 
 abbreviation (iff)
-  iff :: "[bool, bool] \<Rightarrow> bool"  (infixr "<->" 25) where
-  "A <-> B \<equiv> A = B"
-
-notation (xsymbols)
-  iff  (infixr "\<longleftrightarrow>" 25)
+  iff :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<longleftrightarrow>" 25) where
+  "A \<longleftrightarrow> B \<equiv> A = B"
 
 syntax "_The" :: "[pttrn, bool] \<Rightarrow> 'a"  ("(3THE _./ _)" [0, 10] 10)
 translations "THE x. P" \<rightleftharpoons> "CONST The (\<lambda>x. P)"
diff -r 97c06cfd31e5 -r 31f2105521ee src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Dec 27 16:40:09 2015 +0100
+++ b/src/HOL/List.thy	Sun Dec 27 17:16:21 2015 +0100
@@ -3445,7 +3445,7 @@
 lemma remdups_adj_altdef: "(remdups_adj xs = ys) \<longleftrightarrow>
   (\<exists>f::nat => nat. mono f & f ` {0 ..< size xs} = {0 ..< size ys}
     \<and> (\<forall>i < size xs. xs!i = ys!(f i))
-    \<and> (\<forall>i. i + 1 < size xs \<longrightarrow> (xs!i = xs!(i+1) <-> f i = f(i+1))))" (is "?L \<longleftrightarrow> (\<exists>f. ?p f xs ys)")
+    \<and> (\<forall>i. i + 1 < size xs \<longrightarrow> (xs!i = xs!(i+1) \<longleftrightarrow> f i = f(i+1))))" (is "?L \<longleftrightarrow> (\<exists>f. ?p f xs ys)")
 proof
   assume ?L
   then show "\<exists>f. ?p f xs ys"
diff -r 97c06cfd31e5 -r 31f2105521ee src/HOL/Meson.thy
--- a/src/HOL/Meson.thy	Sun Dec 27 16:40:09 2015 +0100
+++ b/src/HOL/Meson.thy	Sun Dec 27 17:16:21 2015 +0100
@@ -22,8 +22,7 @@
   and not_exD: "!!P. ~(\<exists>x. P(x)) ==> \<forall>x. ~P(x)"
   by fast+
 
-text \<open>Removal of \<open>-->\<close> and \<open><->\<close> (positive and
-negative occurrences)\<close>
+text \<open>Removal of \<open>\<longrightarrow>\<close> and \<open>\<longleftrightarrow>\<close> (positive and negative occurrences)\<close>
 
 lemma imp_to_disjD: "P-->Q ==> ~P | Q"
   and not_impD: "~(P-->Q) ==> P & ~Q"
diff -r 97c06cfd31e5 -r 31f2105521ee src/HOL/TLA/Memory/MemoryImplementation.thy
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Sun Dec 27 16:40:09 2015 +0100
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Sun Dec 27 17:16:21 2015 +0100
@@ -33,15 +33,15 @@
 definition
   (* auxiliary predicates *)
   MVOKBARF      :: "Vals \<Rightarrow> bool"
-  where "MVOKBARF v <-> (v : MemVal) | (v = OK) | (v = BadArg) | (v = RPCFailure)"
+  where "MVOKBARF v \<longleftrightarrow> (v : MemVal) | (v = OK) | (v = BadArg) | (v = RPCFailure)"
 
 definition
   MVOKBA        :: "Vals \<Rightarrow> bool"
-  where "MVOKBA v <-> (v : MemVal) | (v = OK) | (v = BadArg)"
+  where "MVOKBA v \<longleftrightarrow> (v : MemVal) | (v = OK) | (v = BadArg)"
 
 definition
   MVNROKBA      :: "Vals \<Rightarrow> bool"
-  where "MVNROKBA v <-> (v : MemVal) | (v = NotAResult) | (v = OK) | (v = BadArg)"
+  where "MVNROKBA v \<longleftrightarrow> (v : MemVal) | (v = NotAResult) | (v = OK) | (v = BadArg)"
 
 definition
   (* tuples of state functions changed by the various components *)
diff -r 97c06cfd31e5 -r 31f2105521ee src/HOL/UNITY/Comp.thy
--- a/src/HOL/UNITY/Comp.thy	Sun Dec 27 16:40:09 2015 +0100
+++ b/src/HOL/UNITY/Comp.thy	Sun Dec 27 17:16:21 2015 +0100
@@ -17,9 +17,9 @@
 instantiation program :: (type) ord
 begin
 
-definition component_def: "F \<le> H <-> (\<exists>G. F\<squnion>G = H)"
+definition component_def: "F \<le> H \<longleftrightarrow> (\<exists>G. F\<squnion>G = H)"
 
-definition strict_component_def: "F < (H::'a program) <-> (F \<le> H & F \<noteq> H)"
+definition strict_component_def: "F < (H::'a program) \<longleftrightarrow> (F \<le> H & F \<noteq> H)"
 
 instance ..
 
diff -r 97c06cfd31e5 -r 31f2105521ee src/HOL/UNITY/Comp/Priority.thy
--- a/src/HOL/UNITY/Comp/Priority.thy	Sun Dec 27 16:40:09 2015 +0100
+++ b/src/HOL/UNITY/Comp/Priority.thy	Sun Dec 27 17:16:21 2015 +0100
@@ -22,11 +22,11 @@
 text{*Following the definitions given in section 4.4 *}
 
 definition highest :: "[vertex, (vertex*vertex)set]=>bool"
-  where "highest i r <-> A i r = {}"
+  where "highest i r \<longleftrightarrow> A i r = {}"
     --{* i has highest priority in r *}
   
 definition lowest :: "[vertex, (vertex*vertex)set]=>bool"
-  where "lowest i r <-> R i r = {}"
+  where "lowest i r \<longleftrightarrow> R i r = {}"
     --{* i has lowest priority in r *}
 
 definition act :: command
diff -r 97c06cfd31e5 -r 31f2105521ee src/HOL/UNITY/Extend.thy
--- a/src/HOL/UNITY/Extend.thy	Sun Dec 27 16:40:09 2015 +0100
+++ b/src/HOL/UNITY/Extend.thy	Sun Dec 27 17:16:21 2015 +0100
@@ -18,7 +18,7 @@
 
 definition
   good_map :: "['a*'b => 'c] => bool"
-  where "good_map h <-> surj h & (\<forall>x y. fst (inv h (h (x,y))) = x)"
+  where "good_map h \<longleftrightarrow> surj h & (\<forall>x y. fst (inv h (h (x,y))) = x)"
      (*Using the locale constant "f", this is  f (h (x,y))) = x*)
   
 definition
diff -r 97c06cfd31e5 -r 31f2105521ee src/HOL/UNITY/Union.thy
--- a/src/HOL/UNITY/Union.thy	Sun Dec 27 16:40:09 2015 +0100
+++ b/src/HOL/UNITY/Union.thy	Sun Dec 27 17:16:21 2015 +0100
@@ -36,7 +36,7 @@
   (*Characterizes safety properties.  Used with specifying Allowed*)
 definition
   safety_prop :: "'a program set => bool"
-  where "safety_prop X <-> SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
+  where "safety_prop X \<longleftrightarrow> SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
 
 syntax
   "_JOIN1" :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion>_./ _)" 10)
diff -r 97c06cfd31e5 -r 31f2105521ee src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Sun Dec 27 16:40:09 2015 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Sun Dec 27 17:16:21 2015 +0100
@@ -538,7 +538,7 @@
   by (cases n) (auto simp del: bintrunc.Suc)
 
 lemma bin_sbin_eq_iff: 
-  "bintrunc (Suc n) x = bintrunc (Suc n) y <-> 
+  "bintrunc (Suc n) x = bintrunc (Suc n) y \<longleftrightarrow> 
    sbintrunc n x = sbintrunc n y"
   apply (rule iffI)
    apply (rule box_equals [OF _ sbintrunc_bintrunc sbintrunc_bintrunc])
@@ -548,7 +548,7 @@
   done
 
 lemma bin_sbin_eq_iff':
-  "0 < n \<Longrightarrow> bintrunc n x = bintrunc n y <-> 
+  "0 < n \<Longrightarrow> bintrunc n x = bintrunc n y \<longleftrightarrow> 
             sbintrunc (n - 1) x = sbintrunc (n - 1) y"
   by (cases n) (simp_all add: bin_sbin_eq_iff del: bintrunc.Suc)
 
diff -r 97c06cfd31e5 -r 31f2105521ee src/HOL/Word/Misc_Typedef.thy
--- a/src/HOL/Word/Misc_Typedef.thy	Sun Dec 27 16:40:09 2015 +0100
+++ b/src/HOL/Word/Misc_Typedef.thy	Sun Dec 27 17:16:21 2015 +0100
@@ -138,7 +138,7 @@
 
 lemmas td = td_thm
 
-lemma set_iff_norm: "w : A <-> w = norm w"
+lemma set_iff_norm: "w : A \<longleftrightarrow> w = norm w"
   by (auto simp: set_Rep_Abs eq_norm' eq_norm [symmetric])
 
 lemma inverse_norm: 
diff -r 97c06cfd31e5 -r 31f2105521ee src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Sun Dec 27 16:40:09 2015 +0100
+++ b/src/HOL/Word/Word.thy	Sun Dec 27 17:16:21 2015 +0100
@@ -1425,7 +1425,7 @@
   apply force
   done
 
-lemma udvd_iff_dvd: "x udvd y <-> unat x dvd unat y"
+lemma udvd_iff_dvd: "x udvd y \<longleftrightarrow> unat x dvd unat y"
   unfolding dvd_def udvd_nat_alt by force
 
 lemmas unat_mono = word_less_nat_alt [THEN iffD1]
@@ -3273,7 +3273,7 @@
 lemma eq_mod_iff: "0 < (n::int) \<Longrightarrow> b = b mod n \<longleftrightarrow> 0 \<le> b \<and> b < n"
   by (simp add: int_mod_lem eq_sym_conv)
 
-lemma mask_eq_iff: "(w AND mask n) = w <-> uint w < 2 ^ n"
+lemma mask_eq_iff: "(w AND mask n) = w \<longleftrightarrow> uint w < 2 ^ n"
   apply (simp add: and_mask_bintr)
   apply (simp add: word_ubin.inverse_norm)
   apply (simp add: eq_mod_iff bintrunc_mod2p min_def)
@@ -3691,7 +3691,7 @@
   done
 
 lemma word_split_bl: "std = size c - size b \<Longrightarrow> 
-    (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c))) <-> 
+    (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c))) \<longleftrightarrow> 
     word_split c = (a, b)"
   apply (rule iffI)
    defer
@@ -3729,7 +3729,7 @@
     (\<forall>n::nat. b !! n \<longleftrightarrow> n < size b \<and> c !! n) \<and> (\<forall>m::nat. a !! m \<longleftrightarrow> m < size a \<and> c !! (m + size b))"
   by (simp add: test_bit_split')
 
-lemma test_bit_split_eq: "word_split c = (a, b) <-> 
+lemma test_bit_split_eq: "word_split c = (a, b) \<longleftrightarrow> 
   ((ALL n::nat. b !! n = (n < size b & c !! n)) &
     (ALL m::nat. a !! m = (m < size a & c !! (m + size b))))"
   apply (rule_tac iffI)