src/Doc/Isar_Ref/HOL_Specific.thy

--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Mar 23 15:54:41 2015 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Mar 23 15:55:41 2015 +0100
@@ -99,8 +99,7 @@
 
   @{rail \<open>
     (@@{command (HOL) inductive} | @@{command (HOL) inductive_set} |
-      @@{command (HOL) coinductive} | @@{command (HOL) coinductive_set})
-    @{syntax target}? \<newline>
+      @@{command (HOL) coinductive} | @@{command (HOL) coinductive_set}) \<newline>
     @{syntax "fixes"} (@'for' @{syntax "fixes"})? (@'where' clauses)? \<newline>
     (@'monos' @{syntax thmrefs})?
     ;
@@ -266,9 +265,9 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{command (HOL) primrec} @{syntax target}? @{syntax "fixes"} @'where' equations
+    @@{command (HOL) primrec} @{syntax "fixes"} @'where' equations
     ;
-    (@@{command (HOL) fun} | @@{command (HOL) function}) @{syntax target}? functionopts?
+    (@@{command (HOL) fun} | @@{command (HOL) function}) functionopts?
       @{syntax "fixes"} \<newline> @'where' equations
     ;
 
@@ -575,8 +574,7 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{command (HOL) partial_function} @{syntax target}?
-      '(' @{syntax nameref} ')' @{syntax "fixes"} \<newline>
+    @@{command (HOL) partial_function} '(' @{syntax nameref} ')' @{syntax "fixes"} \<newline>
       @'where' @{syntax thmdecl}? @{syntax prop}
   \<close>}
 
@@ -1592,25 +1590,25 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{command (HOL) setup_lifting} \<newline>
-      @{syntax thmref} @{syntax thmref}? (@'parametric' @{syntax thmref})?;
+    @@{command (HOL) setup_lifting} @{syntax thmref} @{syntax thmref}? \<newline>
+      (@'parametric' @{syntax thmref})?
   \<close>}
 
   @{rail \<open>
     @@{command (HOL) lift_definition} @{syntax name} '::' @{syntax type}  @{syntax mixfix}? \<newline>
-      'is' @{syntax term} (@'parametric' (@{syntax thmref}+))?;
+      'is' @{syntax term} (@'parametric' (@{syntax thmref}+))?
   \<close>}
 
   @{rail \<open>
-    @@{command (HOL) lifting_forget} @{syntax nameref};
+    @@{command (HOL) lifting_forget} @{syntax nameref}
   \<close>}
 
   @{rail \<open>
-    @@{command (HOL) lifting_update} @{syntax nameref};
+    @@{command (HOL) lifting_update} @{syntax nameref}
   \<close>}
 
   @{rail \<open>
-    @@{attribute (HOL) lifting_restore} @{syntax thmref} (@{syntax thmref} @{syntax thmref})?;
+    @@{attribute (HOL) lifting_restore} @{syntax thmref} (@{syntax thmref} @{syntax thmref})?
   \<close>}
 
   \begin{description}