# HG changeset patch
# User wenzelm
# Date 1152197377 -7200
# Node ID 95aeaa3ef35d9135e6e05e2392f2a3248999b9a1
# Parent  553d48cac687949c580dcda22d960bd91755085c
Isar.context ();

diff -r 553d48cac687 -r 95aeaa3ef35d doc-src/IsarImplementation/Thy/integration.thy
--- a/doc-src/IsarImplementation/Thy/integration.thy	Thu Jul 06 16:49:36 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/integration.thy	Thu Jul 06 16:49:37 2006 +0200
@@ -37,9 +37,9 @@
   @{text theory}, or @{text proof}.  On entering the main Isar loop we
   start with an empty toplevel.  A theory is commenced by giving a
   @{text \<THEORY>} header; within a theory we may issue theory
-  commands such as @{text \<CONSTS>} or @{text \<DEFS>}, or state a
-  @{text \<THEOREM>} to be proven.  Now we are within a proof state,
-  with a rich collection of Isar proof commands for structured proof
+  commands such as @{text \<DEFINITION>}, or state a @{text
+  \<THEOREM>} to be proven.  Now we are within a proof state, with a
+  rich collection of Isar proof commands for structured proof
   composition, or unstructured proof scripts.  When the proof is
   concluded we get back to the theory, which is then updated by
   storing the resulting fact.  Further theory declarations or theorem
@@ -276,6 +276,7 @@
   @{index_ML Isar.main: "unit -> unit"} \\
   @{index_ML Isar.loop: "unit -> unit"} \\
   @{index_ML Isar.state: "unit -> Toplevel.state"} \\
+  @{index_ML Isar.context: "unit -> Proof.context"} \\
   @{index_ML Isar.exn: "unit -> (exn * string) option"} \\
   \end{mldecls}
 
@@ -291,6 +292,9 @@
   toplevel state and optional error condition, respectively.  This
   only works after dropping out of the Isar toplevel loop.
 
+  \item @{ML "Isar.context ()"} produces the proof context from @{ML
+  "Isar.state ()"} above.
+
   \end{description}
 *}