tuned latex
authornipkow
Tue, 04 Feb 2014 21:01:35 +0100
changeset 55320 8a6ee5c1f2e0
parent 55319 e33f25233798
child 55321 eadea363deb6
tuned latex
src/Doc/ProgProve/Bool_nat_list.thy
--- 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))"