discontinued ASCII replacement syntax <->;
authorwenzelm
Sun Dec 27 17:16:21 2015 +0100 (2015-12-27)
changeset 6194131f2105521ee
parent 61940 97c06cfd31e5
child 61942 f02b26f7d39d
discontinued ASCII replacement syntax <->;
NEWS
src/HOL/Fields.thy
src/HOL/HOL.thy
src/HOL/List.thy
src/HOL/Meson.thy
src/HOL/TLA/Memory/MemoryImplementation.thy
src/HOL/UNITY/Comp.thy
src/HOL/UNITY/Comp/Priority.thy
src/HOL/UNITY/Extend.thy
src/HOL/UNITY/Union.thy
src/HOL/Word/Bit_Representation.thy
src/HOL/Word/Misc_Typedef.thy
src/HOL/Word/Word.thy
     1.1 --- a/NEWS	Sun Dec 27 16:40:09 2015 +0100
     1.2 +++ b/NEWS	Sun Dec 27 17:16:21 2015 +0100
     1.3 @@ -474,6 +474,8 @@
     1.4  The subsequent commands help to reproduce the old forms, e.g. to
     1.5  simplify porting old theories:
     1.6  
     1.7 +  notation iff  (infixr "<->" 25)
     1.8 +
     1.9    type_notation Map.map  (infixr "~=>" 0)
    1.10    notation Map.map_comp  (infixl "o'_m" 55)
    1.11  
     2.1 --- a/src/HOL/Fields.thy	Sun Dec 27 16:40:09 2015 +0100
     2.2 +++ b/src/HOL/Fields.thy	Sun Dec 27 17:16:21 2015 +0100
     2.3 @@ -1116,7 +1116,7 @@
     2.4  by (auto simp add: divide_less_eq)
     2.5  
     2.6  lemma divide_less_eq_1_neg [simp]:
     2.7 -  "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"
     2.8 +  "a < 0 \<Longrightarrow> b/a < 1 \<longleftrightarrow> a < b"
     2.9  by (auto simp add: divide_less_eq)
    2.10  
    2.11  lemma eq_divide_eq_1 [simp]:
     3.1 --- a/src/HOL/HOL.thy	Sun Dec 27 16:40:09 2015 +0100
     3.2 +++ b/src/HOL/HOL.thy	Sun Dec 27 17:16:21 2015 +0100
     3.3 @@ -113,11 +113,8 @@
     3.4    not_equal  (infix "\<noteq>" 50)
     3.5  
     3.6  abbreviation (iff)
     3.7 -  iff :: "[bool, bool] \<Rightarrow> bool"  (infixr "<->" 25) where
     3.8 -  "A <-> B \<equiv> A = B"
     3.9 -
    3.10 -notation (xsymbols)
    3.11 -  iff  (infixr "\<longleftrightarrow>" 25)
    3.12 +  iff :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<longleftrightarrow>" 25) where
    3.13 +  "A \<longleftrightarrow> B \<equiv> A = B"
    3.14  
    3.15  syntax "_The" :: "[pttrn, bool] \<Rightarrow> 'a"  ("(3THE _./ _)" [0, 10] 10)
    3.16  translations "THE x. P" \<rightleftharpoons> "CONST The (\<lambda>x. P)"
     4.1 --- a/src/HOL/List.thy	Sun Dec 27 16:40:09 2015 +0100
     4.2 +++ b/src/HOL/List.thy	Sun Dec 27 17:16:21 2015 +0100
     4.3 @@ -3445,7 +3445,7 @@
     4.4  lemma remdups_adj_altdef: "(remdups_adj xs = ys) \<longleftrightarrow>
     4.5    (\<exists>f::nat => nat. mono f & f ` {0 ..< size xs} = {0 ..< size ys}
     4.6      \<and> (\<forall>i < size xs. xs!i = ys!(f i))
     4.7 -    \<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)")
     4.8 +    \<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)")
     4.9  proof
    4.10    assume ?L
    4.11    then show "\<exists>f. ?p f xs ys"
     5.1 --- a/src/HOL/Meson.thy	Sun Dec 27 16:40:09 2015 +0100
     5.2 +++ b/src/HOL/Meson.thy	Sun Dec 27 17:16:21 2015 +0100
     5.3 @@ -22,8 +22,7 @@
     5.4    and not_exD: "!!P. ~(\<exists>x. P(x)) ==> \<forall>x. ~P(x)"
     5.5    by fast+
     5.6  
     5.7 -text \<open>Removal of \<open>-->\<close> and \<open><->\<close> (positive and
     5.8 -negative occurrences)\<close>
     5.9 +text \<open>Removal of \<open>\<longrightarrow>\<close> and \<open>\<longleftrightarrow>\<close> (positive and negative occurrences)\<close>
    5.10  
    5.11  lemma imp_to_disjD: "P-->Q ==> ~P | Q"
    5.12    and not_impD: "~(P-->Q) ==> P & ~Q"
     6.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Sun Dec 27 16:40:09 2015 +0100
     6.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Sun Dec 27 17:16:21 2015 +0100
     6.3 @@ -33,15 +33,15 @@
     6.4  definition
     6.5    (* auxiliary predicates *)
     6.6    MVOKBARF      :: "Vals \<Rightarrow> bool"
     6.7 -  where "MVOKBARF v <-> (v : MemVal) | (v = OK) | (v = BadArg) | (v = RPCFailure)"
     6.8 +  where "MVOKBARF v \<longleftrightarrow> (v : MemVal) | (v = OK) | (v = BadArg) | (v = RPCFailure)"
     6.9  
    6.10  definition
    6.11    MVOKBA        :: "Vals \<Rightarrow> bool"
    6.12 -  where "MVOKBA v <-> (v : MemVal) | (v = OK) | (v = BadArg)"
    6.13 +  where "MVOKBA v \<longleftrightarrow> (v : MemVal) | (v = OK) | (v = BadArg)"
    6.14  
    6.15  definition
    6.16    MVNROKBA      :: "Vals \<Rightarrow> bool"
    6.17 -  where "MVNROKBA v <-> (v : MemVal) | (v = NotAResult) | (v = OK) | (v = BadArg)"
    6.18 +  where "MVNROKBA v \<longleftrightarrow> (v : MemVal) | (v = NotAResult) | (v = OK) | (v = BadArg)"
    6.19  
    6.20  definition
    6.21    (* tuples of state functions changed by the various components *)
     7.1 --- a/src/HOL/UNITY/Comp.thy	Sun Dec 27 16:40:09 2015 +0100
     7.2 +++ b/src/HOL/UNITY/Comp.thy	Sun Dec 27 17:16:21 2015 +0100
     7.3 @@ -17,9 +17,9 @@
     7.4  instantiation program :: (type) ord
     7.5  begin
     7.6  
     7.7 -definition component_def: "F \<le> H <-> (\<exists>G. F\<squnion>G = H)"
     7.8 +definition component_def: "F \<le> H \<longleftrightarrow> (\<exists>G. F\<squnion>G = H)"
     7.9  
    7.10 -definition strict_component_def: "F < (H::'a program) <-> (F \<le> H & F \<noteq> H)"
    7.11 +definition strict_component_def: "F < (H::'a program) \<longleftrightarrow> (F \<le> H & F \<noteq> H)"
    7.12  
    7.13  instance ..
    7.14  
     8.1 --- a/src/HOL/UNITY/Comp/Priority.thy	Sun Dec 27 16:40:09 2015 +0100
     8.2 +++ b/src/HOL/UNITY/Comp/Priority.thy	Sun Dec 27 17:16:21 2015 +0100
     8.3 @@ -22,11 +22,11 @@
     8.4  text{*Following the definitions given in section 4.4 *}
     8.5  
     8.6  definition highest :: "[vertex, (vertex*vertex)set]=>bool"
     8.7 -  where "highest i r <-> A i r = {}"
     8.8 +  where "highest i r \<longleftrightarrow> A i r = {}"
     8.9      --{* i has highest priority in r *}
    8.10    
    8.11  definition lowest :: "[vertex, (vertex*vertex)set]=>bool"
    8.12 -  where "lowest i r <-> R i r = {}"
    8.13 +  where "lowest i r \<longleftrightarrow> R i r = {}"
    8.14      --{* i has lowest priority in r *}
    8.15  
    8.16  definition act :: command
     9.1 --- a/src/HOL/UNITY/Extend.thy	Sun Dec 27 16:40:09 2015 +0100
     9.2 +++ b/src/HOL/UNITY/Extend.thy	Sun Dec 27 17:16:21 2015 +0100
     9.3 @@ -18,7 +18,7 @@
     9.4  
     9.5  definition
     9.6    good_map :: "['a*'b => 'c] => bool"
     9.7 -  where "good_map h <-> surj h & (\<forall>x y. fst (inv h (h (x,y))) = x)"
     9.8 +  where "good_map h \<longleftrightarrow> surj h & (\<forall>x y. fst (inv h (h (x,y))) = x)"
     9.9       (*Using the locale constant "f", this is  f (h (x,y))) = x*)
    9.10    
    9.11  definition
    10.1 --- a/src/HOL/UNITY/Union.thy	Sun Dec 27 16:40:09 2015 +0100
    10.2 +++ b/src/HOL/UNITY/Union.thy	Sun Dec 27 17:16:21 2015 +0100
    10.3 @@ -36,7 +36,7 @@
    10.4    (*Characterizes safety properties.  Used with specifying Allowed*)
    10.5  definition
    10.6    safety_prop :: "'a program set => bool"
    10.7 -  where "safety_prop X <-> SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
    10.8 +  where "safety_prop X \<longleftrightarrow> SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
    10.9  
   10.10  syntax
   10.11    "_JOIN1" :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion>_./ _)" 10)
    11.1 --- a/src/HOL/Word/Bit_Representation.thy	Sun Dec 27 16:40:09 2015 +0100
    11.2 +++ b/src/HOL/Word/Bit_Representation.thy	Sun Dec 27 17:16:21 2015 +0100
    11.3 @@ -538,7 +538,7 @@
    11.4    by (cases n) (auto simp del: bintrunc.Suc)
    11.5  
    11.6  lemma bin_sbin_eq_iff: 
    11.7 -  "bintrunc (Suc n) x = bintrunc (Suc n) y <-> 
    11.8 +  "bintrunc (Suc n) x = bintrunc (Suc n) y \<longleftrightarrow> 
    11.9     sbintrunc n x = sbintrunc n y"
   11.10    apply (rule iffI)
   11.11     apply (rule box_equals [OF _ sbintrunc_bintrunc sbintrunc_bintrunc])
   11.12 @@ -548,7 +548,7 @@
   11.13    done
   11.14  
   11.15  lemma bin_sbin_eq_iff':
   11.16 -  "0 < n \<Longrightarrow> bintrunc n x = bintrunc n y <-> 
   11.17 +  "0 < n \<Longrightarrow> bintrunc n x = bintrunc n y \<longleftrightarrow> 
   11.18              sbintrunc (n - 1) x = sbintrunc (n - 1) y"
   11.19    by (cases n) (simp_all add: bin_sbin_eq_iff del: bintrunc.Suc)
   11.20  
    12.1 --- a/src/HOL/Word/Misc_Typedef.thy	Sun Dec 27 16:40:09 2015 +0100
    12.2 +++ b/src/HOL/Word/Misc_Typedef.thy	Sun Dec 27 17:16:21 2015 +0100
    12.3 @@ -138,7 +138,7 @@
    12.4  
    12.5  lemmas td = td_thm
    12.6  
    12.7 -lemma set_iff_norm: "w : A <-> w = norm w"
    12.8 +lemma set_iff_norm: "w : A \<longleftrightarrow> w = norm w"
    12.9    by (auto simp: set_Rep_Abs eq_norm' eq_norm [symmetric])
   12.10  
   12.11  lemma inverse_norm: 
    13.1 --- a/src/HOL/Word/Word.thy	Sun Dec 27 16:40:09 2015 +0100
    13.2 +++ b/src/HOL/Word/Word.thy	Sun Dec 27 17:16:21 2015 +0100
    13.3 @@ -1425,7 +1425,7 @@
    13.4    apply force
    13.5    done
    13.6  
    13.7 -lemma udvd_iff_dvd: "x udvd y <-> unat x dvd unat y"
    13.8 +lemma udvd_iff_dvd: "x udvd y \<longleftrightarrow> unat x dvd unat y"
    13.9    unfolding dvd_def udvd_nat_alt by force
   13.10  
   13.11  lemmas unat_mono = word_less_nat_alt [THEN iffD1]
   13.12 @@ -3273,7 +3273,7 @@
   13.13  lemma eq_mod_iff: "0 < (n::int) \<Longrightarrow> b = b mod n \<longleftrightarrow> 0 \<le> b \<and> b < n"
   13.14    by (simp add: int_mod_lem eq_sym_conv)
   13.15  
   13.16 -lemma mask_eq_iff: "(w AND mask n) = w <-> uint w < 2 ^ n"
   13.17 +lemma mask_eq_iff: "(w AND mask n) = w \<longleftrightarrow> uint w < 2 ^ n"
   13.18    apply (simp add: and_mask_bintr)
   13.19    apply (simp add: word_ubin.inverse_norm)
   13.20    apply (simp add: eq_mod_iff bintrunc_mod2p min_def)
   13.21 @@ -3691,7 +3691,7 @@
   13.22    done
   13.23  
   13.24  lemma word_split_bl: "std = size c - size b \<Longrightarrow> 
   13.25 -    (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c))) <-> 
   13.26 +    (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c))) \<longleftrightarrow> 
   13.27      word_split c = (a, b)"
   13.28    apply (rule iffI)
   13.29     defer
   13.30 @@ -3729,7 +3729,7 @@
   13.31      (\<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))"
   13.32    by (simp add: test_bit_split')
   13.33  
   13.34 -lemma test_bit_split_eq: "word_split c = (a, b) <-> 
   13.35 +lemma test_bit_split_eq: "word_split c = (a, b) \<longleftrightarrow> 
   13.36    ((ALL n::nat. b !! n = (n < size b & c !! n)) &
   13.37      (ALL m::nat. a !! m = (m < size a & c !! (m + size b))))"
   13.38    apply (rule_tac iffI)