src/HOL/Induct/Com.thy
changeset 24824 b7866aea0815
parent 24178 4ff1dc2aa18d
child 26806 40b411ec05aa
     1.1 --- a/src/HOL/Induct/Com.thy	Wed Oct 03 19:36:05 2007 +0200
     1.2 +++ b/src/HOL/Induct/Com.thy	Wed Oct 03 19:49:33 2007 +0200
     1.3 @@ -11,20 +11,18 @@
     1.4  theory Com imports Main begin
     1.5  
     1.6  typedecl loc
     1.7 -
     1.8  types  state = "loc => nat"
     1.9 -       n2n2n = "nat => nat => nat"
    1.10  
    1.11  datatype
    1.12    exp = N nat
    1.13        | X loc
    1.14 -      | Op n2n2n exp exp
    1.15 +      | Op "nat => nat => nat" exp exp
    1.16        | valOf com exp          ("VALOF _ RESULTIS _"  60)
    1.17  and
    1.18    com = SKIP
    1.19 -      | ":="  loc exp          (infixl  60)
    1.20 -      | Semi  com com          ("_;;_"  [60, 60] 60)
    1.21 -      | Cond  exp com com      ("IF _ THEN _ ELSE _"  60)
    1.22 +      | Assign loc exp         (infixl ":=" 60)
    1.23 +      | Semi com com           ("_;;_"  [60, 60] 60)
    1.24 +      | Cond exp com com       ("IF _ THEN _ ELSE _"  60)
    1.25        | While exp com          ("WHILE _ DO _"  60)
    1.26  
    1.27