now with Goal cmd
authorpaulson
Fri, 17 Jul 1998 10:49:19 +0200
changeset 5153 51bd3cd9ee85
parent 5152 5b63f591678b
child 5154 40fd46f3d3a1
now with Goal cmd
doc-src/Logics/LK-eg.txt
--- a/doc-src/Logics/LK-eg.txt	Thu Jul 16 12:10:56 1998 +0200
+++ b/doc-src/Logics/LK-eg.txt	Fri Jul 17 10:49:19 1998 +0200
@@ -3,7 +3,7 @@
 Pretty.setmargin 72;  (*existing macros just allow this margin*)
 print_depth 0;
 
-Context LK.thy;
+context LK.thy;
 
 Goal "|- EX y. ALL x. P(y)-->P(x)";
 by (resolve_tac [exR] 1);