author | paulson |
Fri, 17 Jul 1998 10:49:19 +0200 | |
changeset 5153 | 51bd3cd9ee85 |
parent 5152 | 5b63f591678b |
child 5154 | 40fd46f3d3a1 |
--- 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);