--- a/NEWS Wed Jan 10 17:21:31 2001 +0100
+++ b/NEWS Wed Jan 10 20:18:55 2001 +0100
@@ -1,22 +1,21 @@
+
Isabelle NEWS -- history user-relevant changes
==============================================
*** Overview of INCOMPATIBILITIES ***
* HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse"
-function;
+operation;
* HOL: induct renamed to lfp_induct;
* HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp;
-* HOL: infix "dvd" now has priority 50 rather than 70
- (because it is a relation)
- infix ^^ has been renamed ``
- infix `` has been renamed `
- "univalent" has been renamed "single_valued"
+* HOL: infix "dvd" now has priority 50 rather than 70 (because it is a
+relation); infix "^^" has been renamed "``"; infix "``" has been
+renamed "`"; "univalent" has been renamed "single_valued";
-* HOLCF: infix ` has been renamed $
+* HOLCF: infix "`" has been renamed "$";
* Isar: 'obtain' no longer declares "that" fact as simp/intro;
@@ -31,9 +30,18 @@
(should now use \isamath{...} and \isatext{...} in custom symbol
definitions);
+* \isabellestyle{NAME} selects version of Isabelle output (currently
+available: are "it" for near math-mode best-style output, "sl" for
+slanted text style, and "tt" for plain type-writer; if no
+\isabellestyle command is given, output is according to slanted
+type-writer);
+
* support sub/super scripts (for single symbols only), input syntax is
like this: "A\<^sup>*" or "A\<^sup>\<star>";
+* some more standard symbols; see Appendix A of the system manual for
+the complete list;
+
* antiquotation @{goals} and @{subgoals} for output of *dynamic* goals
state; Note that presentation of goal states does not conform to
actual human-readable proof documents. Please do not include goal
@@ -62,6 +70,12 @@
* Pure: ?thesis / ?this / "..." now work for pure meta-level
statements as well;
+* Pure: the builtin notion of 'finished' goal now includes the ==-refl
+rule (as well as the assumption rule);
+
+* Pure: 'thm_deps' command visualizes dependencies of theorems and
+lemmas, using the graph browser tool;
+
* HOL: improved method 'induct' --- now handles non-atomic goals
(potential INCOMPATIBILITY); tuned error handling;
@@ -69,6 +83,10 @@
number of facts to be consumed (0 for "type" and 1 for "set" rules);
any remaining facts are inserted into the goal verbatim;
+* HOL: local contexts (aka cases) may now contain term bindings as
+well; the 'cases' and 'induct' methods new provide a ?case binding for
+the result to be shown in each case;
+
* HOL: added 'recdef_tc' command;
@@ -92,6 +110,7 @@
* HOL-Real, HOL-Hyperreals: improved arithmetic simplification;
+
*** CTT ***
* CTT: x-symbol support for Pi, Sigma, -->, : (membership); note that
--- a/doc-src/IsarRef/generic.tex Wed Jan 10 17:21:31 2001 +0100
+++ b/doc-src/IsarRef/generic.tex Wed Jan 10 20:18:55 2001 +0100
@@ -43,7 +43,10 @@
classes involved. After finishing the proof, the theory will be augmented
by a type signature declaration corresponding to the resulting theorem.
\item [$intro_classes$] repeatedly expands all class introduction rules of
- this theory.
+ this theory. Note that this method usually needs not be named explicitly,
+ as it is already included in the default proof step (of $\PROOFNAME$,
+ $\BYNAME$, etc.). In particular, instantiation of trivial (syntactic)
+ classes may be performed by a single ``$\DDOT$'' proof step.
\end{descr}
@@ -737,10 +740,7 @@
\begin{descr}
\item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}
in \cite[\S11]{isabelle-ref}). The optional argument specifies a
- user-supplied search bound (default 20). Note that $blast$ is the only
- classical proof procedure in Isabelle that can handle actual object-logic
- rules as local assumptions ($fast$ etc.\ would just ignore non-atomic
- facts).
+ user-supplied search bound (default 20).
\item [$fast$, $slow$, $best$, $safe$, and $clarify$] refer to the generic
classical reasoner. See \texttt{fast_tac}, \texttt{slow_tac},
\texttt{best_tac}, \texttt{safe_tac}, and \texttt{clarify_tac} in
--- a/doc-src/IsarRef/isar-ref.tex Wed Jan 10 17:21:31 2001 +0100
+++ b/doc-src/IsarRef/isar-ref.tex Wed Jan 10 20:18:55 2001 +0100
@@ -47,6 +47,7 @@
\newcommand{\edrv}{\mathop{\drv}\nolimits}
\newcommand{\Or}{\mathrel{\;|\;}}
+\renewcommand{\vec}[1]{\overline{#1}}
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
--- a/doc-src/IsarRef/pure.tex Wed Jan 10 17:21:31 2001 +0100
+++ b/doc-src/IsarRef/pure.tex Wed Jan 10 20:18:55 2001 +0100
@@ -418,7 +418,7 @@
\item [$\isarkeyword{ML}~text$ and $\isarkeyword{ML_command}~text$] execute ML
commands from $text$. The theory context is passed in the same way as for
- $\isarkeyword{use}$, but may not be changed. Note that
+ $\isarkeyword{use}$, but may not be changed. Note that the output of
$\isarkeyword{ML_command}$ is less verbose than plain $\isarkeyword{ML}$.
\item [$\isarkeyword{ML_setup}~text$] executes ML commands from $text$. The
@@ -543,7 +543,7 @@
\item [$proof(prove)$] means that a new goal has just been stated that is now
to be \emph{proven}; the next command may refine it by some proof method,
and enter a sub-proof to establish the actual result.
-\item [$proof(state)$] is like an internal theory mode: the context may be
+\item [$proof(state)$] is like a nested theory mode: the context may be
augmented by \emph{stating} additional assumptions, intermediate results
etc.
\item [$proof(chain)$] is intermediate between $proof(state)$ and
@@ -693,7 +693,7 @@
of facts in automated proof search.
\item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; thus $\THEN$ is
equivalent to $\FROM{this}$.
-\item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~facts}$; thus the forward
+\item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~this}$; thus the forward
chaining is from earlier facts together with the current ones.
\end{descr}
@@ -1187,7 +1187,8 @@
\subsection{Diagnostics}
-\indexisarcmd{pr}\indexisarcmd{thm}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{typ}
+\indexisarcmd{pr}\indexisarcmd{thm}\indexisarcmd{term}
+\indexisarcmd{prop}\indexisarcmd{typ}
\begin{matharray}{rcl}
\isarcmd{pr}^* & : & \isarkeep{\cdot} \\
\isarcmd{thm}^* & : & \isarkeep{theory~|~proof} \\
@@ -1252,18 +1253,36 @@
\indexisarcmd{print-facts}\indexisarcmd{print-binds}
\indexisarcmd{print-commands}\indexisarcmd{print-syntax}
\indexisarcmd{print-methods}\indexisarcmd{print-attributes}
+\indexisarcmd{thms-containing}\indexisarcmd{thm-deps}
+\indexisarcmd{print-theorems}
\begin{matharray}{rcl}
\isarcmd{print_commands}^* & : & \isarkeep{\cdot} \\
\isarcmd{print_syntax}^* & : & \isarkeep{theory~|~proof} \\
\isarcmd{print_methods}^* & : & \isarkeep{theory~|~proof} \\
\isarcmd{print_attributes}^* & : & \isarkeep{theory~|~proof} \\
+ \isarcmd{print_theorems}^* & : & \isarkeep{theory~|~proof} \\
+ \isarcmd{thms_containing}^* & : & \isarkeep{theory~|~proof} \\
+ \isarcmd{thms_deps}^* & : & \isarkeep{theory~|~proof} \\
\isarcmd{print_facts}^* & : & \isarkeep{proof} \\
\isarcmd{print_binds}^* & : & \isarkeep{proof} \\
\end{matharray}
-These commands print parts of the theory and proof context. Note that there
-are some further ones available, such as for the set of rules declared for
-simplifications.
+\railalias{thmscontaining}{thms\_containing}
+\railterm{thmscontaining}
+
+\railalias{thmdeps}{thm\_deps}
+\railterm{thmdeps}
+
+\begin{rail}
+ thmscontaining (name * )
+ ;
+ thmdeps thmrefs
+ ;
+\end{rail}
+
+These commands print certain parts of the theory and proof context. Note that
+there are some further ones available, such as for the set of rules declared
+for simplifications.
\begin{descr}
\item [$\isarkeyword{print_commands}$] prints Isabelle's outer theory syntax,
@@ -1272,10 +1291,20 @@
terms, depending on the current context. The output can be very verbose,
including grammar tables and syntax translation rules. See \cite[\S7,
\S8]{isabelle-ref} for further information on Isabelle's inner syntax.
-\item [$\isarkeyword{print_methods}$] all proof methods available in the
- current theory context.
-\item [$\isarkeyword{print_attributes}$] all attributes available in the
- current theory context.
+\item [$\isarkeyword{print_methods}$] prints all proof methods available in
+ the current theory context.
+\item [$\isarkeyword{print_attributes}$] prints all attributes available in
+ the current theory context.
+\item [$\isarkeyword{print_theorems}$] prints theorems available in the
+ current theory context. In interactive mode this actually refers to the
+ theorems left by the last transaction; this allows to inspect the result of
+ advanced definitional packages, such as $\isarkeyword{datatype}$.
+\item [$\isarkeyword{thms_containing}~\vec c$] retrieves theorems from the
+ theory context containing all of the constants $\vec c$. Note that giving
+ the empty list yields \emph{all} theorems of the current theory.
+\item [$\isarkeyword{thm_deps}~\vec a$] visualizes dependencies of theorems
+ and lemmas, using Isabelle's graph browser tool (see also
+ \cite{isabelle-sys}).
\item [$\isarkeyword{print_facts}$] prints any named facts of the current
context, including assumptions and local results.
\item [$\isarkeyword{print_binds}$] prints all term abbreviations present in
@@ -1295,7 +1324,7 @@
The Isabelle/Isar top-level maintains a two-stage history, for theory and
proof state transformation. Basically, any command can be undone using
$\isarkeyword{undo}$, excluding mere diagnostic elements. Its effect may be
-revoked via $\isarkeyword{redo}$, unless the corresponding the
+revoked via $\isarkeyword{redo}$, unless the corresponding
$\isarkeyword{undo}$ step has crossed the beginning of a proof or theory. The
$\isarkeyword{kill}$ command aborts the current history node altogether,
discontinuing a proof or even the whole theory. This operation is \emph{not}
--- a/doc-src/IsarRef/syntax.tex Wed Jan 10 17:21:31 2001 +0100
+++ b/doc-src/IsarRef/syntax.tex Wed Jan 10 20:18:55 2001 +0100
@@ -29,7 +29,7 @@
``\texttt{;}'' (semicolon) to separate commands explicitly. This may be
particularly useful in interactive shell sessions to make clear where the
current command is intended to end. Otherwise, the interactive loop will
-continue until end-of-command in clearly indicated from the input syntax,
+continue until end-of-command is clearly indicated from the input syntax,
e.g.\ encounter of the next command keyword.
Advanced interfaces such as Proof~General \cite{proofgeneral} do not require