src/HOL/HOL.thy
changeset 9060 b0dd884b1848
parent 8959 9d793220a46a
child 9352 416b2ecd97a1
     1.1 --- a/src/HOL/HOL.thy	Tue Jun 13 18:33:55 2000 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Jun 13 18:34:59 2000 +0200
     1.3 @@ -93,10 +93,10 @@
     1.4  
     1.5    (* Case expressions *)
     1.6  
     1.7 -  "@case"       :: "['a, cases_syn] => 'b"               ("(case _ of/ _)" 10)
     1.8 -  "@case1"      :: "['a, 'b] => case_syn"                ("(2_ =>/ _)" 10)
     1.9 +  "_case_syntax":: "['a, cases_syn] => 'b"               ("(case _ of/ _)" 10)
    1.10 +  "_case1"      :: "['a, 'b] => case_syn"                ("(2_ =>/ _)" 10)
    1.11    ""            :: "case_syn => cases_syn"               ("_")
    1.12 -  "@case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ | _")
    1.13 +  "_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ | _")
    1.14  
    1.15  translations
    1.16    "x ~= y"                == "~ (x = y)"
    1.17 @@ -119,8 +119,8 @@
    1.18    "ALL "        :: "[idts, bool] => bool"                ("(3\\<forall>_./ _)" [0, 10] 10)
    1.19    "EX "         :: "[idts, bool] => bool"                ("(3\\<exists>_./ _)" [0, 10] 10)
    1.20    "EX! "        :: "[idts, bool] => bool"                ("(3\\<exists>!_./ _)" [0, 10] 10)
    1.21 -  "@case1"      :: "['a, 'b] => case_syn"                ("(2_ \\<Rightarrow>/ _)" 10)
    1.22 -(*"@case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ \\<orelse> _")*)
    1.23 +  "_case1"      :: "['a, 'b] => case_syn"                ("(2_ \\<Rightarrow>/ _)" 10)
    1.24 +(*"_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ \\<orelse> _")*)
    1.25  
    1.26  syntax (symbols output)
    1.27    "op ~="       :: "['a, 'a] => bool"                    ("(_ \\<noteq>/ _)" [51, 51] 50)