equal
deleted
inserted
replaced
353 apply (simp add: Consq_def) |
353 apply (simp add: Consq_def) |
354 done |
354 done |
355 |
355 |
356 lemma Seq_Finite_ind: |
356 lemma Seq_Finite_ind: |
357 "!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a>>s) |] ==> P x" |
357 "!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a>>s) |] ==> P x" |
358 apply (erule (1) sfinite.induct) |
358 apply (erule (1) Finite.induct) |
359 apply (tactic {* def_tac 1 *}) |
359 apply (tactic {* def_tac 1 *}) |
360 apply (simp add: Consq_def) |
360 apply (simp add: Consq_def) |
361 done |
361 done |
362 |
362 |
363 |
363 |