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
```