author | nipkow |
Tue, 04 Feb 2014 21:01:35 +0100 | |
changeset 55320 | 8a6ee5c1f2e0 |
parent 55319 | e33f25233798 |
child 55321 | eadea363deb6 |
--- 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))"