--- a/src/HOL/Modelcheck/MuckeSyn.thy Tue Jun 13 18:33:55 2000 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.thy Tue Jun 13 18:34:59 2000 +0200
@@ -60,10 +60,10 @@
"Mu " :: [idts, 'a pred] => 'a pred ("(3mu _./ _)" 1000)
"Nu " :: [idts, 'a pred] => 'a pred ("(3nu _./ _)" 1000)
- "@case" :: ['a, cases_syn] => 'b ("(case*_* / _ / esac*)" 10)
- "@case1" :: ['a, 'b] => case_syn ("(2*= _ :/ _;)" 10)
+ "_case_syntax":: ['a, cases_syn] => 'b ("(case*_* / _ / esac*)" 10)
+ "_case1" :: ['a, 'b] => case_syn ("(2*= _ :/ _;)" 10)
"" :: case_syn => cases_syn ("_")
- "@case2" :: [case_syn, cases_syn] => cases_syn ("_/ _")
+ "_case2" :: [case_syn, cases_syn] => cases_syn ("_/ _")
(* Terms containing a case statement must be post-processed with the function *)
(* transform_case, defined in MuCalculus.ML. There, all asterikses before the *)
(* "=" will be replaced by the expression between the two asterikses following *)