src/HOL/IMP/Com.thy
changeset 972 e61b058d58d2
parent 965 24eef3860714
child 977 5d57287e5e1e
--- a/src/HOL/IMP/Com.thy	Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/IMP/Com.thy	Fri Mar 24 12:30:35 1995 +0100
@@ -26,9 +26,9 @@
 
 (** Evaluation of arithmetic expressions **)
 consts  evala    :: "(aexp*state*nat)set"
-       "@evala"  :: "[aexp,state,nat] => bool"	("<_,_>/ -a-> _"  [0,0,50] 50)
+       "@evala"  :: "[aexp,state,nat] => bool" ("<_,_>/ -a-> _"  [0,0,50] 50)
 translations
-    "<ae,sig> -a-> n" == "<ae,sig,n> : evala"
+    "<ae,sig> -a-> n" == "(ae,sig,n) : evala"
 inductive "evala"
   intrs 
     N   "<N(n),s> -a-> n"
@@ -51,10 +51,10 @@
 
 (** Evaluation of boolean expressions **)
 consts evalb	:: "(bexp*state*bool)set"	
-       "@evalb" :: "[bexp,state,bool] => bool"	("<_,_>/ -b-> _"  [0,0,50] 50)
+       "@evalb" :: "[bexp,state,bool] => bool" ("<_,_>/ -b-> _"  [0,0,50] 50)
 
 translations
-    "<be,sig> -b-> b" == "<be,sig,b> : evalb"
+    "<be,sig> -b-> b" == "(be,sig,b) : evalb"
 
 inductive "evalb"
  intrs (*avoid clash with ML constructors true, false*)
@@ -79,11 +79,11 @@
 
 (** Execution of commands **)
 consts  evalc    :: "(com*state*state)set"
-        "@evalc" :: "[com,state,state] => bool"  ("<_,_>/ -c-> _" [0,0,50] 50)
-	"assign" :: "[state,nat,loc] => state"   ("_[_'/_]"       [95,0,0] 95)
+        "@evalc" :: "[com,state,state] => bool" ("<_,_>/ -c-> _" [0,0,50] 50)
+	"assign" :: "[state,nat,loc] => state"  ("_[_'/_]"       [95,0,0] 95)
 
 translations
-       "<ce,sig> -c-> s" == "<ce,sig,s> : evalc"
+       "<ce,sig> -c-> s" == "(ce,sig,s) : evalc"
 
 rules 
 	assign_def	"s[m/x] == (%y. if y=x then m else s y)"