src/Doc/ProgProve/Bool_nat_list.thy

 "rev (Cons x xs) = app (rev xs) (Cons x Nil)"
 
 text{* By default, variables @{text xs}, @{text ys} and @{text zs} are of
 @{text list} type.
 
-Command \isacom{value}\indexed{{\sf\textbf{value}}}{value} evaluates a term. For example, *}
+Command \indexed{\isacommand{value}}{value} evaluates a term. For example, *}
 
 value "rev(Cons True (Cons False Nil))"
 
 text{* yields the result @{value "rev(Cons True (Cons False Nil))"}. This works symbolically, too: *}