# HG changeset patch
# User wenzelm
# Date 975611110 -3600
# Node ID 93ca45370c593e673847079016072f8e8e851a9e
# Parent  5e19ae8d9582e9394326c0a1b96990ef19f5b615
schematic goals;

diff -r 5e19ae8d9582 -r 93ca45370c59 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Thu Nov 30 20:04:49 2000 +0100
+++ b/doc-src/IsarRef/pure.tex	Thu Nov 30 20:05:10 2000 +0100
@@ -743,11 +743,29 @@
   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}.
+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}.
+
+\medskip
+
+\begin{warn}
+  Isabelle/Isar suffers theory-level goal statements to contain \emph{unbound
+    schematic variables}, although this does not conform to the aim of
+  human-readable proof documents!  The main problem with schematic goals is
+  that the actual outcome is usually hard to predict, depending on the
+  behavior of the actual proof methods applied during the reasoning.  Note
+  that most semi-automated methods heavily depend on several kinds of implicit
+  rule declarations within the current theory context.  As this would also
+  result in non-compositional checking of sub-proofs, \emph{local goals} are
+  not allowed to be schematic at all.
+  
+  Nevertheless, schematic goals do have their use in Prolog-style interactive
+  synthesis of proven results, usually by stepwise refinement via emulation of
+  traditional Isabelle tactic scripts (see also \S\ref{sec:tactic-commands}).
+  In any case, users should know what they are doing!
+\end{warn}
 
 
 \subsection{Initial and terminal proof steps}\label{sec:proof-steps}