| changeset 20064 | 92aad017b847 |
| parent 20025 | 95aeaa3ef35d |
| child 20447 | 5b75f1c4d7d6 |
--- a/doc-src/IsarImplementation/Thy/integration.thy Sat Jul 08 14:01:31 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/integration.thy Sat Jul 08 14:01:40 2006 +0200 @@ -293,7 +293,7 @@ only works after dropping out of the Isar toplevel loop. \item @{ML "Isar.context ()"} produces the proof context from @{ML - "Isar.state ()"} above. + "Isar.state ()"}. \end{description} *}