--- a/NEWS Fri May 26 18:28:15 2000 +0200
+++ b/NEWS Sun May 28 21:55:50 2000 +0200
@@ -86,6 +86,9 @@
useful for building new logics, but beware of confusion with the
Provers/classical ones;
+* Pure: the local context of (non-atomic) goals is provided via case
+name 'antecedent';
+
* Provers: splitter support (via 'split' attribute and 'simp' method
modifier); 'simp' method: 'only:' modifier removes loopers as well
(including splits);
--- a/doc-src/IsarRef/pure.tex Fri May 26 18:28:15 2000 +0200
+++ b/doc-src/IsarRef/pure.tex Sun May 28 21:55:50 2000 +0200
@@ -681,6 +681,12 @@
also equivalent to $\FROM{this}~\SHOWNAME$.
\end{descr}
+Note that any goal statement causes some term abbreviations (such as
+$\Var{thesis}$, $\dots$) to be bound automatically, see also
+\S\ref{sec:term-abbrev}. Furthermore, the local context of a (non-atomic)
+goal is provided via the case name $antecedent$\indexisarcase{antecedent}, see
+also \S\ref{sec:cases}.
+
\subsection{Initial and terminal proof steps}\label{sec:proof-steps}
--- a/src/Pure/Isar/proof.ML Fri May 26 18:28:15 2000 +0200
+++ b/src/Pure/Isar/proof.ML Sun May 28 21:55:50 2000 +0200
@@ -547,6 +547,8 @@
(* setup goals *)
+val antN = "antecedent";
+
fun setup_goal opt_block prepp kind after_qed name atts raw_propp state =
let
val (state', (prop, gen_binds)) =
@@ -560,6 +562,7 @@
in
state'
|> put_goal (Some (((kind atts, name, prop), ([], goal)), after_qed o map_context gen_binds))
+ |> map_context (ProofContext.add_cases (RuleCases.make goal [antN]))
|> auto_bind_goal prop
|> (if is_chain state then use_facts else reset_facts)
|> new_block