--- a/src/HOL/Isar_examples/KnasterTarski.thy Fri Jul 30 13:43:26 1999 +0200
+++ b/src/HOL/Isar_examples/KnasterTarski.thy Fri Jul 30 13:44:29 1999 +0200
@@ -25,7 +25,7 @@
assume mono: "mono f";
show "f ??a = ??a";
- proof same;
+ proof -;
{{;
fix x;
assume mem: "x : ??H";