equal
deleted
inserted
replaced
190 apply(rule allI)+ |
190 apply(rule allI)+ |
191 apply(induct_tac x xa rule: list_induct2') |
191 apply(induct_tac x xa rule: list_induct2') |
192 apply(simp_all) |
192 apply(simp_all) |
193 done |
193 done |
194 |
194 |
195 |
|
196 (* Rest are unused *) |
|
197 text {* |
|
198 lemma list_rel_refl: |
195 lemma list_rel_refl: |
199 assumes a: "\<And>x y. R x y = (R x = R y)" |
196 assumes a: "\<And>x y. R x y = (R x = R y)" |
200 shows "list_rel R x x" |
197 shows "list_rel R x x" |
201 by (induct x) (auto simp add: a) |
198 by (induct x) (auto simp add: a) |
202 *} |
|
203 |
199 |
204 end |
200 end |