--- a/src/HOL/UNITY/Comp/TimerArray.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/Comp/TimerArray.thy Sat Feb 08 16:05:33 2003 +0100
@@ -18,7 +18,7 @@
"decr == UN n uu. {((Suc n, uu), (n,uu))}"
Timer :: "'a state program"
- "Timer == mk_program (UNIV, {decr}, UNIV)"
+ "Timer == mk_total_program (UNIV, {decr}, UNIV)"
declare Timer_def [THEN def_prg_Init, simp]
@@ -61,8 +61,8 @@
apply (rename_tac "n")
apply (rule PLam_leadsTo_Basis)
apply (auto simp add: lessThan_Suc [symmetric])
-apply (unfold Timer_def, constrains)
-apply (rule_tac act = decr in transientI, auto)
+apply (unfold Timer_def mk_total_program_def, constrains)
+apply (rule_tac act = decr in totalize_transientI, auto)
done
end