src/HOL/HOL.thy
changeset 61955 e96292f32c3c
parent 61941 31f2105521ee
child 62151 dc4c9748a86e
     1.1 --- a/src/HOL/HOL.thy	Mon Dec 28 19:23:15 2015 +0100
     1.2 +++ b/src/HOL/HOL.thy	Mon Dec 28 21:47:32 2015 +0100
     1.3 @@ -73,48 +73,45 @@
     1.4    Trueprop      :: "bool \<Rightarrow> prop"                   ("(_)" 5)
     1.5  
     1.6  axiomatization
     1.7 -  implies       :: "[bool, bool] \<Rightarrow> bool"           (infixr "-->" 25)  and
     1.8 +  implies       :: "[bool, bool] \<Rightarrow> bool"           (infixr "\<longrightarrow>" 25)  and
     1.9    eq            :: "['a, 'a] \<Rightarrow> bool"               (infixl "=" 50)  and
    1.10    The           :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
    1.11  
    1.12  consts
    1.13    True          :: bool
    1.14    False         :: bool
    1.15 -  Not           :: "bool \<Rightarrow> bool"                   ("~ _" [40] 40)
    1.16 +  Not           :: "bool \<Rightarrow> bool"                   ("\<not> _" [40] 40)
    1.17  
    1.18 -  conj          :: "[bool, bool] \<Rightarrow> bool"           (infixr "&" 35)
    1.19 -  disj          :: "[bool, bool] \<Rightarrow> bool"           (infixr "|" 30)
    1.20 +  conj          :: "[bool, bool] \<Rightarrow> bool"           (infixr "\<and>" 35)
    1.21 +  disj          :: "[bool, bool] \<Rightarrow> bool"           (infixr "\<or>" 30)
    1.22  
    1.23 -  All           :: "('a \<Rightarrow> bool) \<Rightarrow> bool"           (binder "ALL " 10)
    1.24 -  Ex            :: "('a \<Rightarrow> bool) \<Rightarrow> bool"           (binder "EX " 10)
    1.25 -  Ex1           :: "('a \<Rightarrow> bool) \<Rightarrow> bool"           (binder "EX! " 10)
    1.26 +  All           :: "('a \<Rightarrow> bool) \<Rightarrow> bool"           (binder "\<forall>" 10)
    1.27 +  Ex            :: "('a \<Rightarrow> bool) \<Rightarrow> bool"           (binder "\<exists>" 10)
    1.28 +  Ex1           :: "('a \<Rightarrow> bool) \<Rightarrow> bool"           (binder "\<exists>!" 10)
    1.29  
    1.30  
    1.31  subsubsection \<open>Additional concrete syntax\<close>
    1.32  
    1.33 -notation (output)
    1.34 -  eq  (infix "=" 50)
    1.35 -
    1.36 -abbreviation
    1.37 -  not_equal :: "['a, 'a] \<Rightarrow> bool"  (infixl "~=" 50) where
    1.38 -  "x ~= y \<equiv> ~ (x = y)"
    1.39 +abbreviation not_equal :: "['a, 'a] \<Rightarrow> bool"  (infixl "\<noteq>" 50)
    1.40 +  where "x \<noteq> y \<equiv> \<not> (x = y)"
    1.41  
    1.42  notation (output)
    1.43 +  eq  (infix "=" 50) and
    1.44 +  not_equal  (infix "\<noteq>" 50)
    1.45 +
    1.46 +notation (ASCII output)
    1.47    not_equal  (infix "~=" 50)
    1.48  
    1.49 -notation (xsymbols)
    1.50 -  Not  ("\<not> _" [40] 40) and
    1.51 -  conj  (infixr "\<and>" 35) and
    1.52 -  disj  (infixr "\<or>" 30) and
    1.53 -  implies  (infixr "\<longrightarrow>" 25) and
    1.54 -  not_equal  (infixl "\<noteq>" 50)
    1.55 -
    1.56 -notation (xsymbols output)
    1.57 -  not_equal  (infix "\<noteq>" 50)
    1.58 +notation (ASCII)
    1.59 +  Not  ("~ _" [40] 40) and
    1.60 +  conj  (infixr "&" 35) and
    1.61 +  disj  (infixr "|" 30) and
    1.62 +  implies  (infixr "-->" 25) and
    1.63 +  not_equal  (infixl "~=" 50)
    1.64  
    1.65  abbreviation (iff)
    1.66 -  iff :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<longleftrightarrow>" 25) where
    1.67 -  "A \<longleftrightarrow> B \<equiv> A = B"
    1.68 +  iff :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<longleftrightarrow>" 25)
    1.69 +  where "A \<longleftrightarrow> B \<equiv> A = B"
    1.70  
    1.71  syntax "_The" :: "[pttrn, bool] \<Rightarrow> 'a"  ("(3THE _./ _)" [0, 10] 10)
    1.72  translations "THE x. P" \<rightleftharpoons> "CONST The (\<lambda>x. P)"
    1.73 @@ -134,16 +131,16 @@
    1.74  nonterminal case_syn and cases_syn
    1.75  syntax
    1.76    "_case_syntax" :: "['a, cases_syn] \<Rightarrow> 'b"  ("(case _ of/ _)" 10)
    1.77 -  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  ("(2_ =>/ _)" 10)
    1.78 +  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  ("(2_ \<Rightarrow>/ _)" 10)
    1.79    "" :: "case_syn \<Rightarrow> cases_syn"  ("_")
    1.80    "_case2" :: "[case_syn, cases_syn] \<Rightarrow> cases_syn"  ("_/ | _")
    1.81 -syntax (xsymbols)
    1.82 -  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  ("(2_ \<Rightarrow>/ _)" 10)
    1.83 +syntax (ASCII)
    1.84 +  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  ("(2_ =>/ _)" 10)
    1.85  
    1.86 -notation (xsymbols)
    1.87 -  All  (binder "\<forall>" 10) and
    1.88 -  Ex  (binder "\<exists>" 10) and
    1.89 -  Ex1  (binder "\<exists>!" 10)
    1.90 +notation (ASCII)
    1.91 +  All  (binder "ALL " 10) and
    1.92 +  Ex  (binder "EX " 10) and
    1.93 +  Ex1  (binder "EX! " 10)
    1.94  
    1.95  notation (HOL)
    1.96    All  (binder "! " 10) and