--- a/src/HOL/HOL.thy Tue Jun 13 18:33:55 2000 +0200
+++ b/src/HOL/HOL.thy Tue Jun 13 18:34:59 2000 +0200
@@ -93,10 +93,10 @@
(* Case expressions *)
- "@case" :: "['a, cases_syn] => 'b" ("(case _ of/ _)" 10)
- "@case1" :: "['a, 'b] => case_syn" ("(2_ =>/ _)" 10)
+ "_case_syntax":: "['a, cases_syn] => 'b" ("(case _ of/ _)" 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" ("_/ | _")
translations
"x ~= y" == "~ (x = y)"
@@ -119,8 +119,8 @@
"ALL " :: "[idts, bool] => bool" ("(3\\<forall>_./ _)" [0, 10] 10)
"EX " :: "[idts, bool] => bool" ("(3\\<exists>_./ _)" [0, 10] 10)
"EX! " :: "[idts, bool] => bool" ("(3\\<exists>!_./ _)" [0, 10] 10)
- "@case1" :: "['a, 'b] => case_syn" ("(2_ \\<Rightarrow>/ _)" 10)
-(*"@case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ \\<orelse> _")*)
+ "_case1" :: "['a, 'b] => case_syn" ("(2_ \\<Rightarrow>/ _)" 10)
+(*"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ \\<orelse> _")*)
syntax (symbols output)
"op ~=" :: "['a, 'a] => bool" ("(_ \\<noteq>/ _)" [51, 51] 50)
--- 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 *)
--- a/src/HOL/Tools/datatype_prop.ML Tue Jun 13 18:33:55 2000 +0200
+++ b/src/HOL/Tools/datatype_prop.ML Tue Jun 13 18:34:59 2000 +0200
@@ -366,7 +366,7 @@
val k = length cargs;
val xs = map (fn i => Variable ("x" ^ string_of_int i)) (i upto i + k - 1);
val t = Variable ("t" ^ string_of_int j);
- val ast = Syntax.mk_appl (Constant "@case1")
+ val ast = Syntax.mk_appl (Constant "_case1")
[Syntax.mk_appl (Constant (Sign.base_name cname)) xs, t];
val ast' = foldr (fn (x, y) =>
Syntax.mk_appl (Constant "_abs") [x, y]) (xs, t)
@@ -374,7 +374,7 @@
(case constrs of
[] => (ast, [ast'])
| cs => let val (ast'', asts) = mk_asts (i + k) (j + 1) cs
- in (Syntax.mk_appl (Constant "@case2") [ast, ast''],
+ in (Syntax.mk_appl (Constant "_case2") [ast, ast''],
ast'::asts)
end)
end;
@@ -382,7 +382,7 @@
fun mk_trrule ((_, (_, _, constrs)), tname) =
let val (ast, asts) = mk_asts 1 1 constrs
in Syntax.ParsePrintRule
- (Syntax.mk_appl (Constant "@case") [Variable "t", ast],
+ (Syntax.mk_appl (Constant "_case_syntax") [Variable "t", ast],
Syntax.mk_appl (Constant (tname ^ "_case"))
(asts @ [Variable "t"]))
end
--- a/src/HOLCF/domain/syntax.ML Tue Jun 13 18:33:55 2000 +0200
+++ b/src/HOLCF/domain/syntax.ML Tue Jun 13 18:34:59 2000 +0200
@@ -70,7 +70,7 @@
fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^
(string_of_int m));
fun app s (l,r) = mk_appl (Constant s) [l,r];
- fun case1 n (con,mx,args) = mk_appl (Constant "@case1")
+ fun case1 n (con,mx,args) = mk_appl (Constant "_case1")
[foldl (app "Rep_CFun") (c_ast con mx, (mapn (argvar n) 1 args)),
expvar n];
fun arg1 n (con,_,args) = if args = [] then expvar n
@@ -78,8 +78,8 @@
[foldr' (app "_idts") (mapn (argvar n) 1 args) , expvar n];
in
ParsePrintRule
- (mk_appl (Constant "@case") [Variable "x", foldr'
- (fn (c,cs) => mk_appl (Constant"@case2") [c,cs])
+ (mk_appl (Constant "_case_syntax") [Variable "x", foldr'
+ (fn (c,cs) => mk_appl (Constant"_case2") [c,cs])
(mapn case1 1 cons')],
mk_appl (Constant "Rep_CFun") [foldl
(fn (w,a ) => mk_appl (Constant"Rep_CFun" ) [w,a ])