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