doc-src/Logics/LK-eg.txt
changeset 5153 51bd3cd9ee85
parent 5151 1e944fe5ce96
--- 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);