# 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);