doc-src/IsarImplementation/Thy/document/Logic.tex
changeset 40255 9ffbc25e1606
parent 40126 916cb4a28ffd
child 40406 313a24b66a8d
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex	Fri Oct 29 11:35:47 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex	Fri Oct 29 11:49:56 2010 +0200
@@ -218,7 +218,7 @@
   ;
   'sort' sort
   ;
-  ('type\_name' | 'type\_abbrev' | 'nonterminal') nameref
+  ('type_name' | 'type_abbrev' | 'nonterminal') nameref
   ;
   'typ' type
   ;
@@ -464,7 +464,7 @@
   \end{matharray}
 
   \begin{rail}
-  ('const\_name' | 'const\_abbrev') nameref
+  ('const_name' | 'const_abbrev') nameref
   ;
   'const' ('(' (type + ',') ')')?
   ;