--- 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)
--- 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]:
--- 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)"
--- 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"
--- 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"
--- 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 *)
--- 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 ..
--- 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
--- 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
--- 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)
--- 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)
--- 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:
--- 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)