--- a/src/Doc/ProgProve/Isar.thy Tue Feb 04 09:04:59 2014 +0000
+++ b/src/Doc/ProgProve/Isar.thy Tue Feb 04 17:38:54 2014 +0100
@@ -76,7 +76,7 @@
\S\ref{sec:forward-proof}---hence the \dots\ in the above grammar. Note
that assumptions, intermediate \isacom{have} statements and global lemmas all
have the same status and are thus collectively referred to as
-\concept{facts}.
+\conceptidx{facts}{fact}.
Fact names can stand for whole lists of facts. For example, if @{text f} is
defined by command \isacom{fun}, @{text"f.simps"} refers to the whole list of
@@ -499,7 +499,7 @@
$\vdots$\\
\isacom{from} @{text "`x>0`"} \dots
\end{quote}
-Note that the quotes around @{text"x>0"} are \concept{back quotes}.
+Note that the quotes around @{text"x>0"} are \conceptnoidx{back quotes}.
They refer to the fact not by name but by value.
\subsection{\isacom{moreover}}