src/HOL/UNITY/Comp/Counter.thy
changeset 42463 f270e3e18be5
parent 36866 426d5781bb25
child 46911 6d2a2f0e904e
     1.1 --- a/src/HOL/UNITY/Comp/Counter.thy	Fri Apr 22 15:57:43 2011 +0200
     1.2 +++ b/src/HOL/UNITY/Comp/Counter.thy	Sat Apr 23 13:00:19 2011 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  
     1.5  (* Variables are names *)
     1.6  datatype name = C | c nat
     1.7 -types state = "name=>int"
     1.8 +type_synonym state = "name=>int"
     1.9  
    1.10  primrec sum  :: "[nat,state]=>int" where
    1.11    (* sum I s = sigma_{i<I}. s (c i) *)
    1.12 @@ -25,7 +25,7 @@
    1.13    "sumj 0 i s = 0"
    1.14  | "sumj (Suc n) i s = (if n=i then sum n s else s (c n) + sumj n i s)"
    1.15    
    1.16 -types command = "(state*state)set"
    1.17 +type_synonym command = "(state*state)set"
    1.18  
    1.19  definition a :: "nat=>command" where
    1.20   "a i = {(s, s'). s'=s(c i:= s (c i) + 1, C:= s C + 1)}"