--- a/doc-src/IsarRef/Thy/document/Proof.tex Fri Oct 29 11:35:47 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Fri Oct 29 11:49:56 2010 +0200
@@ -453,11 +453,11 @@
\begin{rail}
('lemma' | 'theorem' | 'corollary' |
- 'schematic\_lemma' | 'schematic\_theorem' | 'schematic\_corollary') target? (goal | longgoal)
+ 'schematic_lemma' | 'schematic_theorem' | 'schematic_corollary') target? (goal | longgoal)
;
('have' | 'show' | 'hence' | 'thus') goal
;
- 'print\_statement' modes? thmrefs
+ 'print_statement' modes? thmrefs
;
goal: (props + 'and')
@@ -843,7 +843,7 @@
\end{matharray}
\begin{rail}
- ( 'apply' | 'apply\_end' ) method
+ ( 'apply' | 'apply_end' ) method
;
'defer' nat?
;
@@ -903,7 +903,7 @@
\end{matharray}
\begin{rail}
- 'method\_setup' name '=' text text
+ 'method_setup' name '=' text text
;
\end{rail}
@@ -1192,9 +1192,9 @@
caseref: nameref attributes?
;
- 'case\_names' (name +)
+ 'case_names' (name +)
;
- 'case\_conclusion' name (name *)
+ 'case_conclusion' name (name *)
;
'params' ((name *) + 'and')
;