src/HOL/HOL.thy
changeset 11687 b0fe6e522559
parent 11451 8abfb4f7bd02
child 11698 3b3feb92207a
     1.1 --- a/src/HOL/HOL.thy	Thu Oct 04 15:41:43 2001 +0200
     1.2 +++ b/src/HOL/HOL.thy	Thu Oct 04 15:42:48 2001 +0200
     1.3 @@ -77,9 +77,9 @@
     1.4    divide        :: "['a::inverse, 'a] => 'a"        (infixl "'/" 70)
     1.5  
     1.6  syntax (xsymbols)
     1.7 -  abs :: "'a::minus => 'a"    ("\\<bar>_\\<bar>")
     1.8 +  abs :: "'a::minus => 'a"    ("\<bar>_\<bar>")
     1.9  syntax (HTML output)
    1.10 -  abs :: "'a::minus => 'a"    ("\\<bar>_\\<bar>")
    1.11 +  abs :: "'a::minus => 'a"    ("\<bar>_\<bar>")
    1.12  
    1.13  axclass plus_ac0 < plus, zero
    1.14    commute: "x + y = y + x"
    1.15 @@ -118,29 +118,29 @@
    1.16    "let x = a in e"        == "Let a (%x. e)"
    1.17  
    1.18  syntax ("" output)
    1.19 -  "op ="        :: "['a, 'a] => bool"                    ("(_ =/ _)" [51, 51] 50)
    1.20 -  "op ~="       :: "['a, 'a] => bool"                    ("(_ ~=/ _)" [51, 51] 50)
    1.21 +  "="           :: "['a, 'a] => bool"                    (infix 50)
    1.22 +  "~="          :: "['a, 'a] => bool"                    (infix 50)
    1.23  
    1.24  syntax (symbols)
    1.25 -  Not           :: "bool => bool"                        ("\\<not> _" [40] 40)
    1.26 -  "op &"        :: "[bool, bool] => bool"                (infixr "\\<and>" 35)
    1.27 -  "op |"        :: "[bool, bool] => bool"                (infixr "\\<or>" 30)
    1.28 -  "op -->"      :: "[bool, bool] => bool"                (infixr "\\<midarrow>\\<rightarrow>" 25)
    1.29 -  "op ~="       :: "['a, 'a] => bool"                    (infixl "\\<noteq>" 50)
    1.30 -  "ALL "        :: "[idts, bool] => bool"                ("(3\\<forall>_./ _)" [0, 10] 10)
    1.31 -  "EX "         :: "[idts, bool] => bool"                ("(3\\<exists>_./ _)" [0, 10] 10)
    1.32 -  "EX! "        :: "[idts, bool] => bool"                ("(3\\<exists>!_./ _)" [0, 10] 10)
    1.33 -  "_case1"      :: "['a, 'b] => case_syn"                ("(2_ \\<Rightarrow>/ _)" 10)
    1.34 +  Not           :: "bool => bool"                        ("\<not> _" [40] 40)
    1.35 +  "op &"        :: "[bool, bool] => bool"                (infixr "\<and>" 35)
    1.36 +  "op |"        :: "[bool, bool] => bool"                (infixr "\<or>" 30)
    1.37 +  "op -->"      :: "[bool, bool] => bool"                (infixr "\<midarrow>\<rightarrow>" 25)
    1.38 +  "op ~="       :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
    1.39 +  "ALL "        :: "[idts, bool] => bool"                ("(3\<forall>_./ _)" [0, 10] 10)
    1.40 +  "EX "         :: "[idts, bool] => bool"                ("(3\<exists>_./ _)" [0, 10] 10)
    1.41 +  "EX! "        :: "[idts, bool] => bool"                ("(3\<exists>!_./ _)" [0, 10] 10)
    1.42 +  "_case1"      :: "['a, 'b] => case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
    1.43  (*"_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ \\<orelse> _")*)
    1.44  
    1.45  syntax (symbols output)
    1.46 -  "op ~="       :: "['a, 'a] => bool"                    ("(_ \\<noteq>/ _)" [51, 51] 50)
    1.47 +  "op ~="       :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
    1.48  
    1.49  syntax (xsymbols)
    1.50 -  "op -->"      :: "[bool, bool] => bool"                (infixr "\\<longrightarrow>" 25)
    1.51 +  "op -->"      :: "[bool, bool] => bool"                (infixr "\<longrightarrow>" 25)
    1.52  
    1.53  syntax (HTML output)
    1.54 -  Not           :: "bool => bool"                        ("\\<not> _" [40] 40)
    1.55 +  Not           :: "bool => bool"                        ("\<not> _" [40] 40)
    1.56  
    1.57  syntax (HOL)
    1.58    "ALL "        :: "[idts, bool] => bool"                ("(3! _./ _)" [0, 10] 10)
    1.59 @@ -201,6 +201,7 @@
    1.60  (* theory and package setup *)
    1.61  
    1.62  use "HOL_lemmas.ML"
    1.63 +theorems case_split = case_split_thm [case_names True False]
    1.64  
    1.65  declare trans [trans]  (*overridden in theory Calculation*)
    1.66