doc-src/IsarImplementation/Thy/integration.thy
changeset 20064 92aad017b847
parent 20025 95aeaa3ef35d
child 20447 5b75f1c4d7d6
equal deleted inserted replaced
20063:d8d9ea6a6b55 20064:92aad017b847
   291   \item @{ML "Isar.state ()"} and @{ML "Isar.exn ()"} get current
   291   \item @{ML "Isar.state ()"} and @{ML "Isar.exn ()"} get current
   292   toplevel state and optional error condition, respectively.  This
   292   toplevel state and optional error condition, respectively.  This
   293   only works after dropping out of the Isar toplevel loop.
   293   only works after dropping out of the Isar toplevel loop.
   294 
   294 
   295   \item @{ML "Isar.context ()"} produces the proof context from @{ML
   295   \item @{ML "Isar.context ()"} produces the proof context from @{ML
   296   "Isar.state ()"} above.
   296   "Isar.state ()"}.
   297 
   297 
   298   \end{description}
   298   \end{description}
   299 *}
   299 *}
   300 
   300 
   301 
   301