doc-src/Logics/LK-eg.txt
changeset 5153 51bd3cd9ee85
parent 5151 1e944fe5ce96
equal deleted inserted replaced
5152:5b63f591678b 5153:51bd3cd9ee85
     1 (**** LK examples -- process using Doc/tout LK-eg.txt ****)
     1 (**** LK examples -- process using Doc/tout LK-eg.txt ****)
     2 
     2 
     3 Pretty.setmargin 72;  (*existing macros just allow this margin*)
     3 Pretty.setmargin 72;  (*existing macros just allow this margin*)
     4 print_depth 0;
     4 print_depth 0;
     5 
     5 
     6 Context LK.thy;
     6 context LK.thy;
     7 
     7 
     8 Goal "|- EX y. ALL x. P(y)-->P(x)";
     8 Goal "|- EX y. ALL x. P(y)-->P(x)";
     9 by (resolve_tac [exR] 1);
     9 by (resolve_tac [exR] 1);
    10 by (resolve_tac [allR] 1);
    10 by (resolve_tac [allR] 1);
    11 by (resolve_tac [impR] 1);
    11 by (resolve_tac [impR] 1);