src/HOL/HOL.thy
changeset 61941 31f2105521ee
parent 61914 16bfe0a6702d
child 61955 e96292f32c3c
     1.1 --- a/src/HOL/HOL.thy	Sun Dec 27 16:40:09 2015 +0100
     1.2 +++ b/src/HOL/HOL.thy	Sun Dec 27 17:16:21 2015 +0100
     1.3 @@ -113,11 +113,8 @@
     1.4    not_equal  (infix "\<noteq>" 50)
     1.5  
     1.6  abbreviation (iff)
     1.7 -  iff :: "[bool, bool] \<Rightarrow> bool"  (infixr "<->" 25) where
     1.8 -  "A <-> B \<equiv> A = B"
     1.9 -
    1.10 -notation (xsymbols)
    1.11 -  iff  (infixr "\<longleftrightarrow>" 25)
    1.12 +  iff :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<longleftrightarrow>" 25) where
    1.13 +  "A \<longleftrightarrow> B \<equiv> A = B"
    1.14  
    1.15  syntax "_The" :: "[pttrn, bool] \<Rightarrow> 'a"  ("(3THE _./ _)" [0, 10] 10)
    1.16  translations "THE x. P" \<rightleftharpoons> "CONST The (\<lambda>x. P)"