src/Doc/ProgProve/Bool_nat_list.thy
changeset 55320 8a6ee5c1f2e0
parent 55318 908fd015cf2e
child 55465 0d31c0546286
--- a/src/Doc/ProgProve/Bool_nat_list.thy	Tue Feb 04 17:59:33 2014 +0100
+++ b/src/Doc/ProgProve/Bool_nat_list.thy	Tue Feb 04 21:01:35 2014 +0100
@@ -184,7 +184,7 @@
 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))"