| changeset 55389 | 33f833231fa2 |
| parent 55361 | d459a63ca42f |
| child 55417 | 01fbfb60c33e |
--- a/src/Doc/ProgProve/Isar.thy Mon Feb 10 23:24:44 2014 +0100 +++ b/src/Doc/ProgProve/Isar.thy Tue Feb 11 09:29:46 2014 +0100 @@ -372,7 +372,7 @@ then obtain x where p: "P(x)" by blast (*<*)oops(*>*) text{* -After the \isacom{obtain} step, @{text x} (we could have chosen any name) +After the \indexed{\isacom{obtain}}{obtain} step, @{text x} (we could have chosen any name) is a fixed local variable, and @{text p} is the name of the fact \noquotes{@{prop[source] "P(x)"}}.