equal
deleted
inserted
replaced
115 apply(rule conjI) |
115 apply(rule conjI) |
116 apply clarify |
116 apply clarify |
117 apply simp |
117 apply simp |
118 apply clarify |
118 apply clarify |
119 apply simp |
119 apply simp |
120 apply(subgoal_tac "xa=0") |
120 apply(subgoal_tac "x=0") |
121 apply simp |
121 apply simp |
122 apply arith |
122 apply arith |
123 apply clarify |
123 apply clarify |
124 apply(case_tac xaa, simp, simp) |
124 apply(case_tac xa, simp, simp) |
125 apply clarify |
125 apply clarify |
126 apply simp |
126 apply simp |
127 apply(erule_tac x=0 in all_dupE) |
127 apply(erule_tac x=0 in all_dupE) |
128 apply(erule_tac x=1 in allE,simp) |
128 apply(erule_tac x=1 in allE,simp) |
129 apply clarify |
129 apply clarify |