doc-src/IsarRef/Thy/HOL_Specific.thy
changeset 29114 715178f6ae31
parent 29112 f2b45eea6dac
child 29560 fa6c5d62adf5
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Dec 15 21:41:21 2008 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Dec 15 21:54:37 2008 +0100
@@ -812,6 +812,7 @@
   'sledgehammer' (nameref *)
   ;
   'atp\_messages' ('(' nat ')')?
+  ;
 
   'metis' thmrefs
   ;