changeset 14148 | 6580d374a509 |
parent 105 | 216d6ed87399 |
--- a/doc-src/Intro/deriv.txt Wed Aug 13 17:24:59 2003 +0200 +++ b/doc-src/Intro/deriv.txt Wed Aug 13 17:44:01 2003 +0200 @@ -4,7 +4,7 @@ print_depth 0; -val [major,minor] = goal Int_Rule.thy +val [major,minor] = goal IFOL.thy "[| P&Q; [| P; Q |] ==> R |] ==> R"; prth minor; by (resolve_tac [minor] 1);