# HG changeset patch
# User paulson
# Date 831485872 -7200
# Node ID e4f8682eea2e5c4de97de0e9ca1978f7a3ab3f18
# Parent  01beef6262aa8307dec35ebcc01b6ed1fd26fce4
Removal of special syntax for -a-> and -b->

diff -r 01beef6262aa -r e4f8682eea2e src/HOL/IMP/Expr.ML
--- a/src/HOL/IMP/Expr.ML	Tue May 07 18:15:51 1996 +0200
+++ b/src/HOL/IMP/Expr.ML	Tue May 07 18:17:52 1996 +0200
@@ -10,36 +10,36 @@
 open Expr;
 
 val evala_elim_cases = map (evala.mk_cases aexp.simps)
-   ["<N(n),sigma> -a-> i", "<X(x),sigma> -a-> i",
-    "<Op1 f e,sigma> -a-> i", "<Op2 f a1 a2,sigma>  -a-> i"
+   ["(N(n),sigma) -a-> i", "(X(x),sigma) -a-> i",
+    "(Op1 f e,sigma) -a-> i", "(Op2 f a1 a2,sigma)  -a-> i"
    ];
 
 val evalb_elim_cases = map (evalb.mk_cases bexp.simps)
-   ["<true,sigma> -b-> x", "<false,sigma> -b-> x",
-    "<ROp f a0 a1,sigma> -b-> x", "<noti(b),sigma> -b-> x",
-    "<b0 andi b1,sigma> -b-> x", "<b0 ori b1,sigma> -b-> x"
+   ["(true,sigma) -b-> x", "(false,sigma) -b-> x",
+    "(ROp f a0 a1,sigma) -b-> x", "(noti(b),sigma) -b-> x",
+    "(b0 andi b1,sigma) -b-> x", "(b0 ori b1,sigma) -b-> x"
    ];
 
 val evalb_simps = map (fn s => prove_goal Expr.thy s
     (fn _ => [fast_tac (HOL_cs addSIs evalb.intrs addSEs evalb_elim_cases) 1]))
-  ["(<true,sigma> -b-> w) = (w=True)",
-   "(<false,sigma> -b-> w) = (w=False)",
-   "(<ROp f a0 a1,sigma> -b-> w) = \
-\   (? m. <a0,sigma> -a-> m & (? n. <a1,sigma> -a-> n & w = f m n))",
-   "(<noti(b),sigma> -b-> w) = (? x. <b,sigma> -b-> x & w = (~x))",
-   "(<b0 andi b1,sigma> -b-> w) = \
-\   (? x. <b0,sigma> -b-> x & (? y. <b1,sigma> -b-> y & w = (x&y)))",
-   "(<b0 ori b1,sigma> -b-> w) = \
-\   (? x. <b0,sigma> -b-> x & (? y. <b1,sigma> -b-> y & w = (x|y)))"];
+  ["((true,sigma) -b-> w) = (w=True)",
+   "((false,sigma) -b-> w) = (w=False)",
+   "((ROp f a0 a1,sigma) -b-> w) = \
+\   (? m. (a0,sigma) -a-> m & (? n. (a1,sigma) -a-> n & w = f m n))",
+   "((noti(b),sigma) -b-> w) = (? x. (b,sigma) -b-> x & w = (~x))",
+   "((b0 andi b1,sigma) -b-> w) = \
+\   (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x&y)))",
+   "((b0 ori b1,sigma) -b-> w) = \
+\   (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))"];
 
-goal Expr.thy "!n. (<a,s> -a-> n) = (n = A a s)";
+goal Expr.thy "!n. ((a,s) -a-> n) = (n = A a s)";
 by (aexp.induct_tac "a" 1);                               (* struct. ind. *)
 by (ALLGOALS Simp_tac);                                   (* rewr. Den.   *)
 by (TRYALL (fast_tac (set_cs addSIs (evala.intrs@prems)
                              addSEs evala_elim_cases)));
 qed_spec_mp "aexp_iff";
 
-goal Expr.thy "!w. (<b,s> -b-> w) = (w = B b s)";
+goal Expr.thy "!w. ((b,s) -b-> w) = (w = B b s)";
 by (bexp.induct_tac "b" 1);
 by (ALLGOALS(asm_simp_tac (!simpset addcongs [conj_cong]
                                     addsimps (aexp_iff::evalb_simps))));
diff -r 01beef6262aa -r e4f8682eea2e src/HOL/IMP/Expr.thy
--- a/src/HOL/IMP/Expr.thy	Tue May 07 18:15:51 1996 +0200
+++ b/src/HOL/IMP/Expr.thy	Tue May 07 18:17:52 1996 +0200
@@ -24,17 +24,17 @@
        | Op2 n2n2n aexp aexp
 
 (** Evaluation of arithmetic expressions **)
-consts  evala    :: "(aexp*state*nat)set"
-       "@evala"  :: [aexp,state,nat] => bool ("<_,_>/ -a-> _"  [0,0,50] 50)
+consts  evala    :: "((aexp*state) * nat) set"
+       "-a->"    :: "[aexp*state,nat] => bool"         (infixl 50)
 translations
-    "<ae,sig> -a-> n" == "(ae,sig,n) : evala"
+    "aesig -a-> n" == "(aesig,n) : evala"
 inductive "evala"
   intrs 
-    N   "<N(n),s> -a-> n"
-    X   "<X(x),s> -a-> s(x)"
-    Op1 "<e,s> -a-> n ==> <Op1 f e,s> -a-> f(n)"
-    Op2 "[| <e0,s> -a-> n0;  <e1,s>  -a-> n1 |] 
-           ==> <Op2 f e0 e1,s> -a-> f n0 n1"
+    N   "(N(n),s) -a-> n"
+    X   "(X(x),s) -a-> s(x)"
+    Op1 "(e,s) -a-> n ==> (Op1 f e,s) -a-> f(n)"
+    Op2 "[| (e0,s) -a-> n0;  (e1,s)  -a-> n1 |] 
+           ==> (Op2 f e0 e1,s) -a-> f n0 n1"
 
 types n2n2b = "[nat,nat] => bool"
 
@@ -49,23 +49,23 @@
        | ori  bexp bexp         (infixl 60)
 
 (** Evaluation of boolean expressions **)
-consts evalb    :: "(bexp*state*bool)set"       
-       "@evalb" :: [bexp,state,bool] => bool ("<_,_>/ -b-> _"  [0,0,50] 50)
+consts evalb    :: "((bexp*state) * bool)set"       
+       "-b->"   :: "[bexp*state,bool] => bool"         (infixl 50)
 
 translations
-    "<be,sig> -b-> b" == "(be,sig,b) : evalb"
+    "besig -b-> b" == "(besig,b) : evalb"
 
 inductive "evalb"
  intrs (*avoid clash with ML constructors true, false*)
-    tru   "<true,s> -b-> True"
-    fls   "<false,s> -b-> False"
-    ROp   "[| <a0,s> -a-> n0; <a1,s> -a-> n1 |] 
-           ==> <ROp f a0 a1,s> -b-> f n0 n1"
-    noti  "<b,s> -b-> w ==> <noti(b),s> -b-> (~w)"
-    andi  "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] 
-          ==> <b0 andi b1,s> -b-> (w0 & w1)"
-    ori   "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] 
-            ==> <b0 ori b1,s> -b-> (w0 | w1)"
+    tru   "(true,s) -b-> True"
+    fls   "(false,s) -b-> False"
+    ROp   "[| (a0,s) -a-> n0; (a1,s) -a-> n1 |] 
+           ==> (ROp f a0 a1,s) -b-> f n0 n1"
+    noti  "(b,s) -b-> w ==> (noti(b),s) -b-> (~w)"
+    andi  "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |] 
+          ==> (b0 andi b1,s) -b-> (w0 & w1)"
+    ori   "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |] 
+            ==> (b0 ori b1,s) -b-> (w0 | w1)"
 
 (** Denotational semantics of arithemtic and boolean expressions **)
 consts