src/HOL/HOL.thy
changeset 14361 ad2f5da643b4
parent 14357 e49d5d5ae66a
child 14365 3d4df8c166ae
     1.1 --- a/src/HOL/HOL.thy	Sun Jan 25 00:42:22 2004 +0100
     1.2 +++ b/src/HOL/HOL.thy	Mon Jan 26 10:34:02 2004 +0100
     1.3 @@ -96,7 +96,7 @@
     1.4    "EX "         :: "[idts, bool] => bool"                ("(3\<exists>_./ _)" [0, 10] 10)
     1.5    "EX! "        :: "[idts, bool] => bool"                ("(3\<exists>!_./ _)" [0, 10] 10)
     1.6    "_case1"      :: "['a, 'b] => case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
     1.7 -(*"_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ \\<orelse> _")*)
     1.8 +(*"_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ \<orelse> _")*)
     1.9  
    1.10  syntax (xsymbols output)
    1.11    "_not_equal"  :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)