| changeset 12815 | 1f073030b97a |
| parent 11235 | 860c65c7388a |
| child 13238 | a6cb18a25cbb |
--- a/doc-src/TutorialI/Overview/Sets.thy Fri Jan 18 17:46:17 2002 +0100 +++ b/doc-src/TutorialI/Overview/Sets.thy Fri Jan 18 18:30:19 2002 +0100 @@ -102,7 +102,7 @@ theorem "mc f = {s. s \<Turnstile> f}"; apply(induct_tac f); -apply(auto simp add:EF_lemma); +apply(auto simp add: EF_lemma); done; text{*