--- a/src/HOL/Isar_examples/W_correct.thy Thu Sep 30 23:33:41 1999 +0200
+++ b/src/HOL/Isar_examples/W_correct.thy Thu Sep 30 23:37:22 1999 +0200
@@ -82,9 +82,7 @@
theorem W_correct: "W e a n = Ok (s, t, m) ==> $ s a |- e :: t";
proof -;
assume W_ok: "W e a n = Ok (s, t, m)";
- let ?P = "%e. ALL a s t m n . Ok (s, t, m) = W e a n --> $ s a |- e :: t";
- (* FIXME (is ...) fails!? *)
- have "?P e";
+ have "ALL a s t m n . Ok (s, t, m) = W e a n --> $ s a |- e :: t" (is "?P e");
proof (induct e);
fix n; show "?P (Var n)"; by simp;
next;