doc-src/IsarRef/pure.tex
changeset 13016 c039b8ede204
parent 12976 5cfe2941a5db
child 13024 0461b281c2b5
--- a/doc-src/IsarRef/pure.tex	Mon Mar 04 19:08:15 2002 +0100
+++ b/doc-src/IsarRef/pure.tex	Mon Mar 04 22:31:21 2002 +0100
@@ -754,22 +754,22 @@
 (\S\ref{sec:tactic-commands}).\footnote{The $induct$ method covered in
   \S\ref{sec:cases-induct-meth} acts on multiple claims simultaneously.}
 
-Claims at the theory level may be either in ``short'' or ``long'' form.  A
-short goal merely consists of several simultaneous propositions (often just
-one).  A long goal includes an explicit context specification for the
-subsequent conclusions, involving local parameters; here the role of each part
-of the statement is explicitly marked by separate keywords (see also
+Claims at the theory level may be either in short or long form.  A short goal
+merely consists of several simultaneous propositions (often just one).  A long
+goal includes an explicit context specification for the subsequent
+conclusions, involving local parameters; here the role of each part of the
+statement is explicitly marked by separate keywords (see also
 \S\ref{sec:locale}).
 
 \begin{rail}
-  ('lemma' | 'theorem' | 'corollary') locale? (shortgoal | longgoal)
+  ('lemma' | 'theorem' | 'corollary') locale? (goal | longgoal)
   ;
-  ('have' | 'show' | 'hence' | 'thus') shortgoal
+  ('have' | 'show' | 'hence' | 'thus') goal
   ;
   
-  shortgoal: (props + 'and')
+  goal: (props + 'and')
   ;
-  longgoal: thmdecl? (contextelem *) 'shows' shortgoal
+  longgoal: thmdecl? (contextelem *) 'shows' goal
   ;
 \end{rail}