equal
deleted
inserted
replaced
190 apply force |
190 apply force |
191 apply force |
191 apply force |
192 --{* 6 subgoals left *} |
192 --{* 6 subgoals left *} |
193 prefer 6 |
193 prefer 6 |
194 apply(erule_tac x=i in allE) |
194 apply(erule_tac x=i in allE) |
195 apply fastsimp |
195 apply fastforce |
196 --{* 5 subgoals left *} |
196 --{* 5 subgoals left *} |
197 prefer 5 |
197 prefer 5 |
198 apply(case_tac [!] "j=k") |
198 apply(case_tac [!] "j=k") |
199 --{* 10 subgoals left *} |
199 --{* 10 subgoals left *} |
200 apply simp_all |
200 apply simp_all |