equal
deleted
inserted
replaced
222 by (REPEAT_FIRST (eresolve_tac mov_metrics)); |
222 by (REPEAT_FIRST (eresolve_tac mov_metrics)); |
223 by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps @ zcompare_rls))); |
223 by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps @ zcompare_rls))); |
224 by (Blast_tac 1); |
224 by (Blast_tac 1); |
225 qed "E_thm16a"; |
225 qed "E_thm16a"; |
226 |
226 |
227 (*Must sometimes delete them because they introduce multiplication*) |
227 val metric_ss = simpset() addsimps metric_simps; |
228 val metric_ss = simpset() delsimprocs [Int_CC.sum_conv, Int_CC.rel_conv] |
|
229 addsimps metric_simps; |
|
230 |
228 |
231 |
229 |
232 (*lem_lift_5_1 has ~goingup instead of goingdown*) |
230 (*lem_lift_5_1 has ~goingup instead of goingdown*) |
233 Goal "#0<N ==> \ |
231 Goal "#0<N ==> \ |
234 \ Lift : (closed Int Req n Int {s. metric n s = N} Int goingdown) LeadsTo \ |
232 \ Lift : (closed Int Req n Int {s. metric n s = N} Int goingdown) LeadsTo \ |