# HG changeset patch
# User wenzelm
# Date 959543750 -7200
# Node ID dc70b797827f0c842ec091018b8e8618a7dd15d7
# Parent  19956dd3809ea7545576ce82d4699d755c7c7e22
case 'antecedent';

diff -r 19956dd3809e -r dc70b797827f NEWS
--- 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);
diff -r 19956dd3809e -r dc70b797827f doc-src/IsarRef/pure.tex
--- 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}
 
diff -r 19956dd3809e -r dc70b797827f src/Pure/Isar/proof.ML
--- 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