# HG changeset patch
# User paulson
# Date 900665359 -7200
# Node ID 51bd3cd9ee85f7ed4675f5d5b6e20574b5ae6587
# Parent  5b63f591678bd7a946eec4edf80222686d8ff8f9
now with Goal cmd

diff -r 5b63f591678b -r 51bd3cd9ee85 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);