1.1 --- a/NEWS Wed Jan 10 17:21:31 2001 +0100
1.2 +++ b/NEWS Wed Jan 10 20:18:55 2001 +0100
1.3 @@ -1,22 +1,21 @@
1.4 +
1.5 Isabelle NEWS -- history user-relevant changes
1.6 ==============================================
1.7
1.8 *** Overview of INCOMPATIBILITIES ***
1.9
1.10 * HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse"
1.11 -function;
1.12 +operation;
1.13
1.14 * HOL: induct renamed to lfp_induct;
1.15
1.16 * HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp;
1.17
1.18 -* HOL: infix "dvd" now has priority 50 rather than 70
1.19 - (because it is a relation)
1.20 - infix ^^ has been renamed ``
1.21 - infix `` has been renamed `
1.22 - "univalent" has been renamed "single_valued"
1.23 +* HOL: infix "dvd" now has priority 50 rather than 70 (because it is a
1.24 +relation); infix "^^" has been renamed "``"; infix "``" has been
1.25 +renamed "`"; "univalent" has been renamed "single_valued";
1.26
1.27 -* HOLCF: infix ` has been renamed $
1.28 +* HOLCF: infix "`" has been renamed "$";
1.29
1.30 * Isar: 'obtain' no longer declares "that" fact as simp/intro;
1.31
1.32 @@ -31,9 +30,18 @@
1.33 (should now use \isamath{...} and \isatext{...} in custom symbol
1.34 definitions);
1.35
1.36 +* \isabellestyle{NAME} selects version of Isabelle output (currently
1.37 +available: are "it" for near math-mode best-style output, "sl" for
1.38 +slanted text style, and "tt" for plain type-writer; if no
1.39 +\isabellestyle command is given, output is according to slanted
1.40 +type-writer);
1.41 +
1.42 * support sub/super scripts (for single symbols only), input syntax is
1.43 like this: "A\<^sup>*" or "A\<^sup>\<star>";
1.44
1.45 +* some more standard symbols; see Appendix A of the system manual for
1.46 +the complete list;
1.47 +
1.48 * antiquotation @{goals} and @{subgoals} for output of *dynamic* goals
1.49 state; Note that presentation of goal states does not conform to
1.50 actual human-readable proof documents. Please do not include goal
1.51 @@ -62,6 +70,12 @@
1.52 * Pure: ?thesis / ?this / "..." now work for pure meta-level
1.53 statements as well;
1.54
1.55 +* Pure: the builtin notion of 'finished' goal now includes the ==-refl
1.56 +rule (as well as the assumption rule);
1.57 +
1.58 +* Pure: 'thm_deps' command visualizes dependencies of theorems and
1.59 +lemmas, using the graph browser tool;
1.60 +
1.61 * HOL: improved method 'induct' --- now handles non-atomic goals
1.62 (potential INCOMPATIBILITY); tuned error handling;
1.63
1.64 @@ -69,6 +83,10 @@
1.65 number of facts to be consumed (0 for "type" and 1 for "set" rules);
1.66 any remaining facts are inserted into the goal verbatim;
1.67
1.68 +* HOL: local contexts (aka cases) may now contain term bindings as
1.69 +well; the 'cases' and 'induct' methods new provide a ?case binding for
1.70 +the result to be shown in each case;
1.71 +
1.72 * HOL: added 'recdef_tc' command;
1.73
1.74
1.75 @@ -92,6 +110,7 @@
1.76
1.77 * HOL-Real, HOL-Hyperreals: improved arithmetic simplification;
1.78
1.79 +
1.80 *** CTT ***
1.81
1.82 * CTT: x-symbol support for Pi, Sigma, -->, : (membership); note that
2.1 --- a/doc-src/IsarRef/generic.tex Wed Jan 10 17:21:31 2001 +0100
2.2 +++ b/doc-src/IsarRef/generic.tex Wed Jan 10 20:18:55 2001 +0100
2.3 @@ -43,7 +43,10 @@
2.4 classes involved. After finishing the proof, the theory will be augmented
2.5 by a type signature declaration corresponding to the resulting theorem.
2.6 \item [$intro_classes$] repeatedly expands all class introduction rules of
2.7 - this theory.
2.8 + this theory. Note that this method usually needs not be named explicitly,
2.9 + as it is already included in the default proof step (of $\PROOFNAME$,
2.10 + $\BYNAME$, etc.). In particular, instantiation of trivial (syntactic)
2.11 + classes may be performed by a single ``$\DDOT$'' proof step.
2.12 \end{descr}
2.13
2.14
2.15 @@ -737,10 +740,7 @@
2.16 \begin{descr}
2.17 \item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}
2.18 in \cite[\S11]{isabelle-ref}). The optional argument specifies a
2.19 - user-supplied search bound (default 20). Note that $blast$ is the only
2.20 - classical proof procedure in Isabelle that can handle actual object-logic
2.21 - rules as local assumptions ($fast$ etc.\ would just ignore non-atomic
2.22 - facts).
2.23 + user-supplied search bound (default 20).
2.24 \item [$fast$, $slow$, $best$, $safe$, and $clarify$] refer to the generic
2.25 classical reasoner. See \texttt{fast_tac}, \texttt{slow_tac},
2.26 \texttt{best_tac}, \texttt{safe_tac}, and \texttt{clarify_tac} in
3.1 --- a/doc-src/IsarRef/isar-ref.tex Wed Jan 10 17:21:31 2001 +0100
3.2 +++ b/doc-src/IsarRef/isar-ref.tex Wed Jan 10 20:18:55 2001 +0100
3.3 @@ -47,6 +47,7 @@
3.4 \newcommand{\edrv}{\mathop{\drv}\nolimits}
3.5 \newcommand{\Or}{\mathrel{\;|\;}}
3.6
3.7 +\renewcommand{\vec}[1]{\overline{#1}}
3.8
3.9 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
3.10
4.1 --- a/doc-src/IsarRef/pure.tex Wed Jan 10 17:21:31 2001 +0100
4.2 +++ b/doc-src/IsarRef/pure.tex Wed Jan 10 20:18:55 2001 +0100
4.3 @@ -418,7 +418,7 @@
4.4
4.5 \item [$\isarkeyword{ML}~text$ and $\isarkeyword{ML_command}~text$] execute ML
4.6 commands from $text$. The theory context is passed in the same way as for
4.7 - $\isarkeyword{use}$, but may not be changed. Note that
4.8 + $\isarkeyword{use}$, but may not be changed. Note that the output of
4.9 $\isarkeyword{ML_command}$ is less verbose than plain $\isarkeyword{ML}$.
4.10
4.11 \item [$\isarkeyword{ML_setup}~text$] executes ML commands from $text$. The
4.12 @@ -543,7 +543,7 @@
4.13 \item [$proof(prove)$] means that a new goal has just been stated that is now
4.14 to be \emph{proven}; the next command may refine it by some proof method,
4.15 and enter a sub-proof to establish the actual result.
4.16 -\item [$proof(state)$] is like an internal theory mode: the context may be
4.17 +\item [$proof(state)$] is like a nested theory mode: the context may be
4.18 augmented by \emph{stating} additional assumptions, intermediate results
4.19 etc.
4.20 \item [$proof(chain)$] is intermediate between $proof(state)$ and
4.21 @@ -693,7 +693,7 @@
4.22 of facts in automated proof search.
4.23 \item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; thus $\THEN$ is
4.24 equivalent to $\FROM{this}$.
4.25 -\item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~facts}$; thus the forward
4.26 +\item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~this}$; thus the forward
4.27 chaining is from earlier facts together with the current ones.
4.28 \end{descr}
4.29
4.30 @@ -1187,7 +1187,8 @@
4.31
4.32 \subsection{Diagnostics}
4.33
4.34 -\indexisarcmd{pr}\indexisarcmd{thm}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{typ}
4.35 +\indexisarcmd{pr}\indexisarcmd{thm}\indexisarcmd{term}
4.36 +\indexisarcmd{prop}\indexisarcmd{typ}
4.37 \begin{matharray}{rcl}
4.38 \isarcmd{pr}^* & : & \isarkeep{\cdot} \\
4.39 \isarcmd{thm}^* & : & \isarkeep{theory~|~proof} \\
4.40 @@ -1252,18 +1253,36 @@
4.41 \indexisarcmd{print-facts}\indexisarcmd{print-binds}
4.42 \indexisarcmd{print-commands}\indexisarcmd{print-syntax}
4.43 \indexisarcmd{print-methods}\indexisarcmd{print-attributes}
4.44 +\indexisarcmd{thms-containing}\indexisarcmd{thm-deps}
4.45 +\indexisarcmd{print-theorems}
4.46 \begin{matharray}{rcl}
4.47 \isarcmd{print_commands}^* & : & \isarkeep{\cdot} \\
4.48 \isarcmd{print_syntax}^* & : & \isarkeep{theory~|~proof} \\
4.49 \isarcmd{print_methods}^* & : & \isarkeep{theory~|~proof} \\
4.50 \isarcmd{print_attributes}^* & : & \isarkeep{theory~|~proof} \\
4.51 + \isarcmd{print_theorems}^* & : & \isarkeep{theory~|~proof} \\
4.52 + \isarcmd{thms_containing}^* & : & \isarkeep{theory~|~proof} \\
4.53 + \isarcmd{thms_deps}^* & : & \isarkeep{theory~|~proof} \\
4.54 \isarcmd{print_facts}^* & : & \isarkeep{proof} \\
4.55 \isarcmd{print_binds}^* & : & \isarkeep{proof} \\
4.56 \end{matharray}
4.57
4.58 -These commands print parts of the theory and proof context. Note that there
4.59 -are some further ones available, such as for the set of rules declared for
4.60 -simplifications.
4.61 +\railalias{thmscontaining}{thms\_containing}
4.62 +\railterm{thmscontaining}
4.63 +
4.64 +\railalias{thmdeps}{thm\_deps}
4.65 +\railterm{thmdeps}
4.66 +
4.67 +\begin{rail}
4.68 + thmscontaining (name * )
4.69 + ;
4.70 + thmdeps thmrefs
4.71 + ;
4.72 +\end{rail}
4.73 +
4.74 +These commands print certain parts of the theory and proof context. Note that
4.75 +there are some further ones available, such as for the set of rules declared
4.76 +for simplifications.
4.77
4.78 \begin{descr}
4.79 \item [$\isarkeyword{print_commands}$] prints Isabelle's outer theory syntax,
4.80 @@ -1272,10 +1291,20 @@
4.81 terms, depending on the current context. The output can be very verbose,
4.82 including grammar tables and syntax translation rules. See \cite[\S7,
4.83 \S8]{isabelle-ref} for further information on Isabelle's inner syntax.
4.84 -\item [$\isarkeyword{print_methods}$] all proof methods available in the
4.85 - current theory context.
4.86 -\item [$\isarkeyword{print_attributes}$] all attributes available in the
4.87 - current theory context.
4.88 +\item [$\isarkeyword{print_methods}$] prints all proof methods available in
4.89 + the current theory context.
4.90 +\item [$\isarkeyword{print_attributes}$] prints all attributes available in
4.91 + the current theory context.
4.92 +\item [$\isarkeyword{print_theorems}$] prints theorems available in the
4.93 + current theory context. In interactive mode this actually refers to the
4.94 + theorems left by the last transaction; this allows to inspect the result of
4.95 + advanced definitional packages, such as $\isarkeyword{datatype}$.
4.96 +\item [$\isarkeyword{thms_containing}~\vec c$] retrieves theorems from the
4.97 + theory context containing all of the constants $\vec c$. Note that giving
4.98 + the empty list yields \emph{all} theorems of the current theory.
4.99 +\item [$\isarkeyword{thm_deps}~\vec a$] visualizes dependencies of theorems
4.100 + and lemmas, using Isabelle's graph browser tool (see also
4.101 + \cite{isabelle-sys}).
4.102 \item [$\isarkeyword{print_facts}$] prints any named facts of the current
4.103 context, including assumptions and local results.
4.104 \item [$\isarkeyword{print_binds}$] prints all term abbreviations present in
4.105 @@ -1295,7 +1324,7 @@
4.106 The Isabelle/Isar top-level maintains a two-stage history, for theory and
4.107 proof state transformation. Basically, any command can be undone using
4.108 $\isarkeyword{undo}$, excluding mere diagnostic elements. Its effect may be
4.109 -revoked via $\isarkeyword{redo}$, unless the corresponding the
4.110 +revoked via $\isarkeyword{redo}$, unless the corresponding
4.111 $\isarkeyword{undo}$ step has crossed the beginning of a proof or theory. The
4.112 $\isarkeyword{kill}$ command aborts the current history node altogether,
4.113 discontinuing a proof or even the whole theory. This operation is \emph{not}
5.1 --- a/doc-src/IsarRef/syntax.tex Wed Jan 10 17:21:31 2001 +0100
5.2 +++ b/doc-src/IsarRef/syntax.tex Wed Jan 10 20:18:55 2001 +0100
5.3 @@ -29,7 +29,7 @@
5.4 ``\texttt{;}'' (semicolon) to separate commands explicitly. This may be
5.5 particularly useful in interactive shell sessions to make clear where the
5.6 current command is intended to end. Otherwise, the interactive loop will
5.7 -continue until end-of-command in clearly indicated from the input syntax,
5.8 +continue until end-of-command is clearly indicated from the input syntax,
5.9 e.g.\ encounter of the next command keyword.
5.10
5.11 Advanced interfaces such as Proof~General \cite{proofgeneral} do not require