| changeset 28823 | dcbef866c9e2 |
| parent 27681 | 8cedebf55539 |
| child 29234 | 60f7fb56f8cd |
--- a/src/HOL/ex/Tarski.thy Mon Nov 17 17:00:27 2008 +0100 +++ b/src/HOL/ex/Tarski.thy Mon Nov 17 17:00:55 2008 +0100 @@ -923,6 +923,6 @@ apply (rule fixf_po, clarify) apply (simp add: P_def A_def r_def) apply (rule Tarski.tarski_full_lemma [OF Tarski.intro [OF _ Tarski_axioms.intro]]) -proof - show "CLF cl f" by unfold_locales qed +proof - show "CLF cl f" .. qed end