src/HOL/IMP/Com.thy
changeset 9241 f961c1fdff50
parent 8029 05446a898852
child 12338 de0f4a63baa5
--- a/src/HOL/IMP/Com.thy	Tue Jul 04 10:54:32 2000 +0200
+++ b/src/HOL/IMP/Com.thy	Tue Jul 04 10:54:46 2000 +0200
@@ -9,18 +9,18 @@
 
 Com = Main +
 
-types 
-      val
+types
       loc
-      state = "loc => val"
-      aexp  = "state => val"
+      val   = nat (* or anything else, nat used in examples *)
+      state = loc => val
+      aexp  = state => val
       bexp  = state => bool
 
-arities loc,val :: term
+arities loc :: term
 
 datatype
   com = SKIP
-      | ":="  loc aexp         (infixl  60)
+      | ":=="  loc aexp         (infixl  60)
       | Semi  com com          ("_; _"  [60, 60] 10)
       | Cond  bexp com com     ("IF _ THEN _ ELSE _"  60)
       | While bexp com         ("WHILE _ DO _"  60)