1.1 --- a/doc-src/Ref/defining.tex	Tue Jul 28 16:30:56 1998 +0200
     1.2 +++ b/doc-src/Ref/defining.tex	Tue Jul 28 16:33:43 1998 +0200
     1.3 @@ -799,7 +799,7 @@
     1.4  After loading this definition from the file {\tt Hilbert.thy}, you can
     1.5  start to prove theorems in the logic:
     1.6  \begin{ttbox}
     1.7 -goal Hilbert.thy "P --> P";
     1.8 +Goal "P --> P";
     1.9  {\out Level 0}
    1.10  {\out P --> P}
    1.11  {\out  1.  P --> P}
    1.12 @@ -880,7 +880,7 @@
    1.13  \end{ttbox}
    1.14  Now we can prove mixed theorems like
    1.15  \begin{ttbox}
    1.16 -goal MinIFC.thy "P & False --> Q";
    1.17 +Goal "P & False --> Q";
    1.18  by (resolve_tac [MinI.impI] 1);
    1.19  by (dresolve_tac [MinC.conjE2] 1);
    1.20  by (eresolve_tac [MinIF.FalseE] 1);