| changeset 12815 | 1f073030b97a |
| parent 11293 | 6878bb02a7f9 |
| child 13249 | 4b3de6370184 |
--- a/doc-src/TutorialI/Overview/Ind.thy Fri Jan 18 17:46:17 2002 +0100 +++ b/doc-src/TutorialI/Overview/Ind.thy Fri Jan 18 18:30:19 2002 +0100 @@ -93,7 +93,7 @@ lemma "wf{(x,y). (x,y) \<in> r \<and> y \<in> acc r}" thm wfI apply(rule_tac A = "acc r" in wfI) - apply (blast elim:acc.elims) + apply (blast elim: acc.elims) apply(simp(no_asm_use)) thm acc.induct apply(erule acc.induct)