# HG changeset patch
# User wenzelm
# Date 1434998318 -7200
# Node ID e7003c8041e2adb4e34bfebbb83a6edf275ec8be
# Parent  51a6997b13841c8675c09638de4dfafd8bdb0f60
tuned;

diff -r 51a6997b1384 -r e7003c8041e2 src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Mon Jun 22 20:36:33 2015 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy	Mon Jun 22 20:38:38 2015 +0200
@@ -73,14 +73,14 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{method sleep} @{syntax real}
-    ;
     (@@{method fold} | @@{method unfold} | @@{method insert}) @{syntax thmrefs}
     ;
     (@@{method erule} | @@{method drule} | @@{method frule})
       ('(' @{syntax nat} ')')? @{syntax thmrefs}
     ;
     (@@{method intro} | @@{method elim}) @{syntax thmrefs}?
+    ;
+    @@{method sleep} @{syntax real}
   \<close>}
 
   \begin{description}