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