--- a/src/HOL/UNITY/TimerArray.thy Wed Feb 16 15:04:12 2000 +0100
+++ b/src/HOL/UNITY/TimerArray.thy Fri Feb 18 15:20:44 2000 +0100
@@ -8,11 +8,16 @@
TimerArray = PPROD +
+types 'a state = "nat * 'a" (*second component allows new variables*)
+
constdefs
- decr :: "(nat*nat) set"
- "decr == UN n. {(Suc n, n)}"
+ count :: "'a state => nat"
+ "count s == fst s"
- Timer :: nat program
+ decr :: "('a state * 'a state) set"
+ "decr == UN n uu. {((Suc n, uu), (n,uu))}"
+
+ Timer :: 'a state program
"Timer == mk_program (UNIV, {decr})"
end