rename @case to _case_syntax (improves on low-level errors);
authorwenzelm
Tue Jun 13 18:34:59 2000 +0200 (2000-06-13)
changeset 9060b0dd884b1848
parent 9059 2b537d9e6f49
child 9061 144b06e6729e
rename @case to _case_syntax (improves on low-level errors);
src/HOL/HOL.thy
src/HOL/Modelcheck/MuckeSyn.thy
src/HOL/Tools/datatype_prop.ML
src/HOLCF/domain/syntax.ML
     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)
     2.1 --- a/src/HOL/Modelcheck/MuckeSyn.thy	Tue Jun 13 18:33:55 2000 +0200
     2.2 +++ b/src/HOL/Modelcheck/MuckeSyn.thy	Tue Jun 13 18:34:59 2000 +0200
     2.3 @@ -60,10 +60,10 @@
     2.4    "Mu "		:: [idts, 'a pred] => 'a pred		("(3mu _./ _)" 1000)
     2.5    "Nu "		:: [idts, 'a pred] => 'a pred		("(3nu _./ _)" 1000)
     2.6    
     2.7 -  "@case"       :: ['a, cases_syn] => 'b            ("(case*_* / _ / esac*)" 10)
     2.8 -  "@case1"      :: ['a, 'b] => case_syn             ("(2*= _ :/ _;)" 10)
     2.9 +  "_case_syntax":: ['a, cases_syn] => 'b            ("(case*_* / _ / esac*)" 10)
    2.10 +  "_case1"      :: ['a, 'b] => case_syn             ("(2*= _ :/ _;)" 10)
    2.11    ""            :: case_syn => cases_syn            ("_")
    2.12 -  "@case2"      :: [case_syn, cases_syn] => cases_syn   ("_/ _")
    2.13 +  "_case2"      :: [case_syn, cases_syn] => cases_syn   ("_/ _")
    2.14  (* Terms containing a case statement must be post-processed with the function  *)
    2.15  (* transform_case, defined in MuCalculus.ML. There, all asterikses before the  *)
    2.16  (* "=" will be replaced by the expression between the two asterikses following *)
     3.1 --- a/src/HOL/Tools/datatype_prop.ML	Tue Jun 13 18:33:55 2000 +0200
     3.2 +++ b/src/HOL/Tools/datatype_prop.ML	Tue Jun 13 18:34:59 2000 +0200
     3.3 @@ -366,7 +366,7 @@
     3.4          val k = length cargs;
     3.5          val xs = map (fn i => Variable ("x" ^ string_of_int i)) (i upto i + k - 1);
     3.6          val t = Variable ("t" ^ string_of_int j);
     3.7 -        val ast = Syntax.mk_appl (Constant "@case1")
     3.8 +        val ast = Syntax.mk_appl (Constant "_case1")
     3.9            [Syntax.mk_appl (Constant (Sign.base_name cname)) xs, t];
    3.10          val ast' = foldr (fn (x, y) =>
    3.11            Syntax.mk_appl (Constant "_abs") [x, y]) (xs, t)
    3.12 @@ -374,7 +374,7 @@
    3.13          (case constrs of
    3.14              [] => (ast, [ast'])
    3.15            | cs => let val (ast'', asts) = mk_asts (i + k) (j + 1) cs
    3.16 -              in (Syntax.mk_appl (Constant "@case2") [ast, ast''],
    3.17 +              in (Syntax.mk_appl (Constant "_case2") [ast, ast''],
    3.18                    ast'::asts)
    3.19                end)
    3.20        end;
    3.21 @@ -382,7 +382,7 @@
    3.22      fun mk_trrule ((_, (_, _, constrs)), tname) =
    3.23        let val (ast, asts) = mk_asts 1 1 constrs
    3.24        in Syntax.ParsePrintRule
    3.25 -        (Syntax.mk_appl (Constant "@case") [Variable "t", ast],
    3.26 +        (Syntax.mk_appl (Constant "_case_syntax") [Variable "t", ast],
    3.27           Syntax.mk_appl (Constant (tname ^ "_case"))
    3.28             (asts @ [Variable "t"]))
    3.29        end
     4.1 --- a/src/HOLCF/domain/syntax.ML	Tue Jun 13 18:33:55 2000 +0200
     4.2 +++ b/src/HOLCF/domain/syntax.ML	Tue Jun 13 18:34:59 2000 +0200
     4.3 @@ -70,7 +70,7 @@
     4.4  	fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^
     4.5  					 (string_of_int m));
     4.6  	fun app s (l,r)   = mk_appl (Constant s) [l,r];
     4.7 -	fun case1 n (con,mx,args) = mk_appl (Constant "@case1")
     4.8 +	fun case1 n (con,mx,args) = mk_appl (Constant "_case1")
     4.9  		 [foldl (app "Rep_CFun") (c_ast con mx, (mapn (argvar n) 1 args)),
    4.10  		  expvar n];
    4.11  	fun arg1 n (con,_,args) = if args = [] then expvar n 
    4.12 @@ -78,8 +78,8 @@
    4.13  		 [foldr' (app "_idts") (mapn (argvar n) 1 args) , expvar n];
    4.14    in
    4.15      ParsePrintRule
    4.16 -      (mk_appl (Constant "@case") [Variable "x", foldr'
    4.17 -				(fn (c,cs) => mk_appl (Constant"@case2") [c,cs])
    4.18 +      (mk_appl (Constant "_case_syntax") [Variable "x", foldr'
    4.19 +				(fn (c,cs) => mk_appl (Constant"_case2") [c,cs])
    4.20  				 (mapn case1 1 cons')],
    4.21         mk_appl (Constant "Rep_CFun") [foldl 
    4.22  				(fn (w,a ) => mk_appl (Constant"Rep_CFun" ) [w,a ])