# HG changeset patch
# User wenzelm
# Date 1738876216 -3600
# Node ID df68d656d5c46d4013f37f3af4f629c759c3f2f9
# Parent  a3a8bd0cd172a2c41a22e7c18e9bf04565ab68ff
more accurate rail diagram (amending de9d43c427ae);

diff -r a3a8bd0cd172 -r df68d656d5c4 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Feb 06 17:29:03 2025 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Feb 06 22:10:16 2025 +0100
@@ -1653,7 +1653,6 @@
     ;
 
     @@{command (HOL) try0} ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' @{syntax thms} ) + ) ?
-      @{syntax nat}?
     ;
 
     @@{command (HOL) sledgehammer} ( '[' args ']' )? facts? @{syntax nat}?