equal
deleted
inserted
replaced
118 apply clarify |
118 apply clarify |
119 apply simp |
119 apply simp |
120 apply clarify |
120 apply clarify |
121 apply simp |
121 apply simp |
122 apply(subgoal_tac "j=0") |
122 apply(subgoal_tac "j=0") |
123 apply (rotate_tac -1) |
123 apply (simp) |
124 apply (simp (asm_lr)) |
|
125 apply arith |
124 apply arith |
126 apply clarify |
125 apply clarify |
127 apply(case_tac i,simp,simp) |
126 apply(case_tac i,simp,simp) |
128 apply clarify |
127 apply clarify |
129 apply simp |
128 apply simp |
130 apply(erule_tac x=0 in all_dupE) |
129 apply(erule_tac x=0 in all_dupE) |
131 apply(erule_tac x=1 in allE,simp) |
130 apply(erule_tac x=1 in allE,simp) |
132 apply clarify |
131 apply clarify |
133 apply(case_tac i,simp) |
132 apply(case_tac i,simp) |