--- 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)