doc-src/Intro/deriv.txt
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);