# HG changeset patch
# User paulson
# Date 831635153 -7200
# Node ID 8b3de497b49dc8c794181ec0b829d7645da53627
# Parent  b50755328aadc70d281db3effc85fc54adec0edd
Removed special syntax for -a-> and nested tuples to left

diff -r b50755328aad -r 8b3de497b49d src/ZF/IMP/Com.thy
--- a/src/ZF/IMP/Com.thy	Thu May 09 11:45:00 1996 +0200
+++ b/src/ZF/IMP/Com.thy	Thu May 09 11:45:53 1996 +0200
@@ -23,11 +23,11 @@
 
 (** Evaluation of arithmetic expressions **)
 consts  evala    :: i
-       "@evala"  :: [i,i,i] => o                ("<_,_>/ -a-> _"  [0,0,50] 50)
+        "-a->"   :: [i,i] => o                  (infixl 50)
 translations
-    "<ae,sig> -a-> n" == "<ae,sig,n> : evala"
+    "p -a-> n" == "<p,n> : evala"
 inductive
-  domains "evala" <= "aexp * (loc -> nat) * nat"
+  domains "evala" <= "(aexp * (loc -> nat)) * nat"
   intrs 
     N   "[| n:nat;  sigma:loc->nat |] ==> <N(n),sigma> -a-> n"
     X   "[| x:loc;  sigma:loc->nat |] ==> <X(x),sigma> -a-> sigma`x"
@@ -52,13 +52,13 @@
 
 (** Evaluation of boolean expressions **)
 consts evalb    :: i    
-       "@evalb" :: [i,i,i] => o         ("<_,_>/ -b-> _" [0,0,50] 50)
+       "-b->"   :: [i,i] => o                   (infixl 50)
 
 translations
-    "<be,sig> -b-> b" == "<be,sig,b> : evalb"
+    "p -b-> b" == "<p,b> : evalb"
 
 inductive
-  domains "evalb" <= "bexp * (loc -> nat) * bool"
+  domains "evalb" <= "(bexp * (loc -> nat)) * bool"
   intrs (*avoid clash with ML constructors true, false*)
     tru   "[| sigma:loc -> nat |] ==> <true,sigma> -b-> 1"
     fls   "[| sigma:loc -> nat |] ==> <false,sigma> -b-> 0"
@@ -90,17 +90,17 @@
 
 (** Execution of commands **)
 consts  evalc    :: i
-        "@evalc" :: [i,i,i] => o                ("<_,_>/ -c-> _" [0,0,50] 50)
-        "assign" :: [i,i,i] => i                ("_[_'/_]"       [95,0,0] 95)
+        "-c->"   :: [i,i] => o                   (infixl 50)
+        "assign" :: [i,i,i] => i                 ("_[_'/_]"       [95,0,0] 95)
 
 translations
-       "<ce,sig> -c-> s" == "<ce,sig,s> : evalc"
+       "p -c-> s" == "<p,s> : evalc"
 
 defs 
         assign_def      "sigma[m/x] == lam y:loc. if(y=x,m,sigma`y)"
 
 inductive
-  domains "evalc" <= "com * (loc -> nat) * (loc -> nat)"
+  domains "evalc" <= "(com * (loc -> nat)) * (loc -> nat)"
   intrs
     skip    "[| sigma: loc -> nat |] ==> <skip,sigma> -c-> sigma"