# HG changeset patch
# User wenzelm
# Date 1436176493 -7200
# Node ID 402aafa3d9cc4cafd87a250c924cf27dc84f7db1
# Parent  4ac91718cc27a0a1befb4914e5f9da25ff8f076e
tuned;

diff -r 4ac91718cc27 -r 402aafa3d9cc src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Jul 06 11:48:56 2015 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Jul 06 11:54:53 2015 +0200
@@ -1465,22 +1465,15 @@
   @{rail \<open>
     @@{command (HOL) setup_lifting} @{syntax thmref} @{syntax thmref}? \<newline>
       (@'parametric' @{syntax thmref})?
-  \<close>}
-
-  @{rail \<open>
-    @@{command (HOL) lift_definition} ('(' 'code_dt' ')')? @{syntax name} '::' @{syntax type}  \<newline>
-      @{syntax mixfix}? 'is' @{syntax term} (@'parametric' (@{syntax thmref}+))?
-  \<close>}
-
-  @{rail \<open>
+    ;
+    @@{command (HOL) lift_definition} ('(' 'code_dt' ')')? \<newline>
+      @{syntax name} '::' @{syntax type} @{syntax mixfix}? 'is' @{syntax term} \<newline>
+      (@'parametric' (@{syntax thmref}+))?
+    ;
     @@{command (HOL) lifting_forget} @{syntax nameref}
-  \<close>}
-
-  @{rail \<open>
+    ;
     @@{command (HOL) lifting_update} @{syntax nameref}
-  \<close>}
-
-  @{rail \<open>
+    ;
     @@{attribute (HOL) lifting_restore} @{syntax thmref} (@{syntax thmref} @{syntax thmref})?
   \<close>}