changeset 32960 | 69916a850301 |
parent 31974 | e81979a703a4 |
child 36319 | 8feb2c4bef1a |
--- a/src/FOL/ex/Classical.thy Sat Oct 17 01:05:59 2009 +0200 +++ b/src/FOL/ex/Classical.thy Sat Oct 17 14:43:18 2009 +0200 @@ -418,7 +418,7 @@ by fast text{*Halting problem: Formulation of Li Dafa (AAR Newsletter 27, Oct 1994.) - author U. Egly*} + author U. Egly*} lemma "((\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z)))) --> (\<exists>w. C(w) & (\<forall>y. C(y) --> (\<forall>z. D(w,y,z))))) &