src/HOL/UNITY/Comp/TimerArray.thy
changeset 42463 f270e3e18be5
parent 37936 1e4c5015a72e
child 61943 7fba644ed827
     1.1 --- a/src/HOL/UNITY/Comp/TimerArray.thy	Fri Apr 22 15:57:43 2011 +0200
     1.2 +++ b/src/HOL/UNITY/Comp/TimerArray.thy	Sat Apr 23 13:00:19 2011 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  theory TimerArray imports "../UNITY_Main" begin
     1.6  
     1.7 -types 'a state = "nat * 'a"   (*second component allows new variables*)
     1.8 +type_synonym 'a state = "nat * 'a"   (*second component allows new variables*)
     1.9  
    1.10  definition count :: "'a state => nat"
    1.11    where "count s = fst s"