equal
deleted
inserted
replaced
24 by (rtac preservesI 1); |
24 by (rtac preservesI 1); |
25 by (constrains_tac 1); |
25 by (constrains_tac 1); |
26 qed "Timer_preserves_snd"; |
26 qed "Timer_preserves_snd"; |
27 AddIffs [Timer_preserves_snd]; |
27 AddIffs [Timer_preserves_snd]; |
28 |
28 |
|
29 Addsimps [PLam_stable]; |
29 |
30 |
30 Goal "finite I \ |
31 Goal "finite I \ |
31 \ ==> (plam i: I. Timer) : UNIV leadsTo {(s,uu). ALL i:I. s i = 0}"; |
32 \ ==> (plam i: I. Timer) : UNIV leadsTo {(s,uu). ALL i:I. s i = 0}"; |
32 by (eres_inst_tac [("A'1", "%i. lift_set i ({0} <*> UNIV)")] |
33 by (eres_inst_tac [("A'1", "%i. lift_set i ({0} <*> UNIV)")] |
33 (finite_stable_completion RS leadsTo_weaken) 1); |
34 (finite_stable_completion RS leadsTo_weaken) 1); |