equal
deleted
inserted
replaced
273 done |
273 done |
274 |
274 |
275 lemma Finite_cons_a: "Finite x --> a~=UU --> x=a##xs --> Finite xs" |
275 lemma Finite_cons_a: "Finite x --> a~=UU --> x=a##xs --> Finite xs" |
276 apply (intro strip) |
276 apply (intro strip) |
277 apply (erule Finite.cases) |
277 apply (erule Finite.cases) |
278 apply fastsimp |
278 apply fastforce |
279 apply simp |
279 apply simp |
280 done |
280 done |
281 |
281 |
282 lemma Finite_cons: "a~=UU ==>(Finite (a##x)) = (Finite x)" |
282 lemma Finite_cons: "a~=UU ==>(Finite (a##x)) = (Finite x)" |
283 apply (rule iffI) |
283 apply (rule iffI) |