equal
deleted
inserted
replaced
98 EVERY' [rtac ctxt mp, rtac ctxt map_cong0, |
98 EVERY' [rtac ctxt mp, rtac ctxt map_cong0, |
99 CONJ_WRAP' (K (rtac ctxt ballI THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1; |
99 CONJ_WRAP' (K (rtac ctxt ballI THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1; |
100 |
100 |
101 fun mk_map_cong0L_tac ctxt passive map_cong0 map_id = |
101 fun mk_map_cong0L_tac ctxt passive map_cong0 map_id = |
102 (rtac ctxt trans THEN' rtac ctxt map_cong0 THEN' EVERY' (replicate passive (rtac ctxt refl))) 1 THEN |
102 (rtac ctxt trans THEN' rtac ctxt map_cong0 THEN' EVERY' (replicate passive (rtac ctxt refl))) 1 THEN |
103 REPEAT_DETERM (EVERY' [rtac ctxt trans, etac ctxt bspec, atac, rtac ctxt sym, rtac ctxt @{thm id_apply}] 1) THEN |
103 REPEAT_DETERM (EVERY' [rtac ctxt trans, etac ctxt bspec, assume_tac ctxt, |
|
104 rtac ctxt sym, rtac ctxt @{thm id_apply}] 1) THEN |
104 rtac ctxt map_id 1; |
105 rtac ctxt map_id 1; |
105 |
106 |
106 end; |
107 end; |