src/HOL/UNITY/Comp/TimerArray.thy
changeset 61943 7fba644ed827
parent 42463 f270e3e18be5
child 67613 ce654b0e6d69
     1.1 --- a/src/HOL/UNITY/Comp/TimerArray.thy	Sun Dec 27 21:46:36 2015 +0100
     1.2 +++ b/src/HOL/UNITY/Comp/TimerArray.thy	Sun Dec 27 22:07:17 2015 +0100
     1.3 @@ -42,7 +42,7 @@
     1.4  lemma TimerArray_leadsTo_zero:
     1.5       "finite I  
     1.6        ==> (plam i: I. Timer) : UNIV leadsTo {(s,uu). ALL i:I. s i = 0}"
     1.7 -apply (erule_tac A'1 = "%i. lift_set i ({0} <*> UNIV)" 
     1.8 +apply (erule_tac A'1 = "%i. lift_set i ({0} \<times> UNIV)" 
     1.9         in finite_stable_completion [THEN leadsTo_weaken])
    1.10  apply auto
    1.11  (*Safety property, already reduced to the single Timer case*)
    1.12 @@ -51,7 +51,7 @@
    1.13  (*Progress property for the array of Timers*)
    1.14  apply (rule_tac f = "sub i o fst" in lessThan_induct)
    1.15  apply (case_tac "m")
    1.16 -(*Annoying need to massage the conditions to have the form (... <*> UNIV)*)
    1.17 +(*Annoying need to massage the conditions to have the form (... \<times> UNIV)*)
    1.18  apply (auto intro: subset_imp_leadsTo 
    1.19          simp add: insert_absorb 
    1.20                    lift_set_Un_distrib [symmetric] lessThan_Suc [symmetric]