--- a/ANNOUNCE Tue Nov 24 10:33:02 2009 +0100
+++ b/ANNOUNCE Tue Nov 24 10:33:21 2009 +0100
@@ -7,7 +7,34 @@
file in the distribution for more details. Some important changes
are:
-* FIXME
+* Isabelle tool "wwwfind" provides web interface for 'find_theorems'
+on a given logic image.
+
+* HOL-SMT: proof method "smt" for a combination of first-order logic
+with equality, linear and nonlinear (natural/integer/real) arithmetic,
+and fixed-size bitvectors.
+
+* HOL-Boogie: an interactive prover back-end for Boogie and VCC.
+
+* HOL: Counterexample generator tool Nitpick based on the Kodkod
+relational model finder.
+
+* HOL: predicate compiler turning inductive into (executable)
+equational specifications.
+
+* HOL: refined number theory.
+
+* HOL: various parts of multivariate analysis.
+
+* HOLCF: new definitional domain package.
+
+* Revised tutorial on locales.
+
+* Support for Poly/ML 5.3.0, with improved reporting of compiler
+errors and run-time exceptions, including detailed source positions.
+
+* Parallel checking of nested Isar proofs, with improved scalability
+up to 8 cores.
You may get Isabelle2009-1 from the following mirror sites:
--- a/Admin/E/README Tue Nov 24 10:33:02 2009 +0100
+++ b/Admin/E/README Tue Nov 24 10:33:21 2009 +0100
@@ -1,4 +1,3 @@
-
This distribution of E 1.0-004 has been compiled according to the
README included in the official version from
http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html
@@ -8,23 +7,12 @@
$ ./configure
$ make
-The resulting PROVER/eproof executable has been changed to be
-relocatable:
-
- $ diff eproof-orig eproof
- 1c1
- < #!/bin/bash -f
- ---
- > #!/usr/bin/env bash
- 3c3,4
- < EXECPATH=/Users/schulz/SOURCES/Projects/E/PROVER
- ---
- > set -o noglob
- > EXECPATH="$(cd "$(dirname "$0")"; pwd)"
+The PROVER/eproof executable has been replaced by a version written in
+perl (by Sascha Boehme).
Now the main executables in PROVER/ are moved to the platform-specific
target directory (E/x86-linux etc.).
- Makarius
- 07-Apr-2009
+ Makarius
+ 23-Nov-2009
--- a/INSTALL Tue Nov 24 10:33:02 2009 +0100
+++ b/INSTALL Tue Nov 24 10:33:21 2009 +0100
@@ -17,7 +17,7 @@
site installation of Isabelle on Linux/x86 works like this:
tar -C /usr/local -xzf Isabelle.tar.gz
- tar -C /usr/local -xzf polyml_x86-linux.tar.gz
+ tar -C /usr/local -xzf polyml.tar.gz
tar -C /usr/local -xzf HOL_x86-linux.tar.gz
The install prefix given above may be changed as appropriate; there is
--- a/NEWS Tue Nov 24 10:33:02 2009 +0100
+++ b/NEWS Tue Nov 24 10:33:21 2009 +0100
@@ -114,19 +114,17 @@
fixpoint theorem.
* Reorganization of number theory, INCOMPATIBILITY:
- - new number theory development for nat and int, in
- theories Divides and GCD as well as in new session
- Number_Theory
- - some constants and facts now suffixed with _nat and
- _int accordingly
- - former session NumberTheory now named Old_Number_Theory,
- including theories Legacy_GCD and Primes (prefer Number_Theory
- if possible)
+ - new number theory development for nat and int, in theories Divides
+ and GCD as well as in new session Number_Theory
+ - some constants and facts now suffixed with _nat and _int
+ accordingly
+ - former session NumberTheory now named Old_Number_Theory, including
+ theories Legacy_GCD and Primes (prefer Number_Theory if possible)
- moved theory Pocklington from src/HOL/Library to
src/HOL/Old_Number_Theory
-* Theory GCD includes functions Gcd/GCD and Lcm/LCM for the gcd and lcm
-of finite and infinite sets. It is shown that they form a complete
+* Theory GCD includes functions Gcd/GCD and Lcm/LCM for the gcd and
+lcm of finite and infinite sets. It is shown that they form a complete
lattice.
* Class semiring_div requires superclass no_zero_divisors and proof of
@@ -198,8 +196,6 @@
abbreviation for "inv_into UNIV". Lemmas are renamed accordingly.
INCOMPATIBILITY.
---
-
* Most rules produced by inductive and datatype package have mandatory
prefixes. INCOMPATIBILITY.
@@ -208,8 +204,9 @@
DERIV_intros assumes composition with an additional function and
matches a variable to the derivative, which has to be solved by the
Simplifier. Hence (auto intro!: DERIV_intros) computes the derivative
-of most elementary terms. Former Maclauren.DERIV_tac and Maclauren.deriv_tac
-should be replaced by (auto intro!: DERIV_intros). INCOMPATIBILITY.
+of most elementary terms. Former Maclauren.DERIV_tac and
+Maclauren.deriv_tac should be replaced by (auto intro!: DERIV_intros).
+INCOMPATIBILITY.
* Code generator attributes follow the usual underscore convention:
code_unfold replaces code unfold
@@ -274,7 +271,8 @@
* The 'fixrec' package now supports "bottom patterns". Bottom
patterns can be used to generate strictness rules, or to make
functions more strict (much like the bang-patterns supported by the
-Glasgow Haskell Compiler). See src/HOLCF/ex/Fixrec_ex.thy for examples.
+Glasgow Haskell Compiler). See src/HOLCF/ex/Fixrec_ex.thy for
+examples.
*** ML ***
--- a/doc-src/IsarRef/Thy/Spec.thy Tue Nov 24 10:33:02 2009 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy Tue Nov 24 10:33:21 2009 +0100
@@ -456,13 +456,10 @@
\secref{sec:object-logic}). Separate introduction rules @{text
loc_axioms.intro} and @{text loc.intro} are provided as well.
- \item @{command "print_locale"}~@{text "import + body"} prints the
- specified locale expression in a flattened form. The notable
- special case @{command "print_locale"}~@{text loc} just prints the
- contents of the named locale, but keep in mind that type-inference
- will normalize type variables according to the usual alphabetical
- order. The command omits @{element "notes"} elements by default.
- Use @{command "print_locale"}@{text "!"} to get them included.
+ \item @{command "print_locale"}~@{text "locale"} prints the
+ contents of the named locale. The command omits @{element "notes"}
+ elements by default. Use @{command "print_locale"}@{text "!"} to
+ have them included.
\item @{command "print_locales"} prints the names of all locales
of the current theory.
@@ -537,7 +534,7 @@
qualifier, although only for fragments of @{text expr} that are not
interpreted in the theory already.
- \item @{command "interpretation"}~@{text "expr insts \<WHERE> eqns"}
+ \item @{command "interpretation"}~@{text "expr \<WHERE> eqns"}
interprets @{text expr} in the theory. The command generates proof
obligations for the instantiated specifications (assumes and defines
elements). Once these are discharged by the user, instantiated
@@ -563,19 +560,24 @@
interpretations dynamically participate in any facts added to
locales.
- \item @{command "interpret"}~@{text "expr insts"}
+ \item @{command "interpret"}~@{text "expr"}
interprets @{text expr} in the proof context and is otherwise
similar to interpretation in theories.
+ \item @{command "print_interps"}~@{text "locale"} lists all
+ interpretations of @{text "locale"} in the current theory, including
+ those due to a combination of an @{command "interpretation"} and
+ one or several @{command "sublocale"} declarations.
+
\end{description}
\begin{warn}
Since attributes are applied to interpreted theorems,
interpretation may modify the context of common proof tools, e.g.\
- the Simplifier or Classical Reasoner. Since the behavior of such
- automated reasoning tools is \emph{not} stable under
- interpretation morphisms, manual declarations might have to be
- added to revert such declarations.
+ the Simplifier or Classical Reasoner. As the behavior of such
+ tools is \emph{not} stable under interpretation morphisms, manual
+ declarations might have to be added to the target context of the
+ interpretation to revert such declarations.
\end{warn}
\begin{warn}
--- a/doc-src/IsarRef/Thy/document/Spec.tex Tue Nov 24 10:33:02 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Tue Nov 24 10:33:21 2009 +0100
@@ -478,13 +478,10 @@
\isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} by \isa{{\isachardoublequote}{\isasymlongrightarrow}{\isachardoublequote}} in HOL; see also
\secref{sec:object-logic}). Separate introduction rules \isa{loc{\isacharunderscore}axioms{\isachardot}intro} and \isa{loc{\isachardot}intro} are provided as well.
- \item \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}import\ {\isacharplus}\ body{\isachardoublequote}} prints the
- specified locale expression in a flattened form. The notable
- special case \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{loc} just prints the
- contents of the named locale, but keep in mind that type-inference
- will normalize type variables according to the usual alphabetical
- order. The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}} elements by default.
- Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to get them included.
+ \item \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}locale{\isachardoublequote}} prints the
+ contents of the named locale. The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}}
+ elements by default. Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to
+ have them included.
\item \hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}} prints the names of all locales
of the current theory.
@@ -559,7 +556,7 @@
qualifier, although only for fragments of \isa{expr} that are not
interpreted in the theory already.
- \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}
+ \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ {\isasymWHERE}\ eqns{\isachardoublequote}}
interprets \isa{expr} in the theory. The command generates proof
obligations for the instantiated specifications (assumes and defines
elements). Once these are discharged by the user, instantiated
@@ -585,19 +582,24 @@
interpretations dynamically participate in any facts added to
locales.
- \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr\ insts{\isachardoublequote}}
+ \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr{\isachardoublequote}}
interprets \isa{expr} in the proof context and is otherwise
similar to interpretation in theories.
+ \item \hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}~\isa{{\isachardoublequote}locale{\isachardoublequote}} lists all
+ interpretations of \isa{{\isachardoublequote}locale{\isachardoublequote}} in the current theory, including
+ those due to a combination of an \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} and
+ one or several \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}} declarations.
+
\end{description}
\begin{warn}
Since attributes are applied to interpreted theorems,
interpretation may modify the context of common proof tools, e.g.\
- the Simplifier or Classical Reasoner. Since the behavior of such
- automated reasoning tools is \emph{not} stable under
- interpretation morphisms, manual declarations might have to be
- added to revert such declarations.
+ the Simplifier or Classical Reasoner. As the behavior of such
+ tools is \emph{not} stable under interpretation morphisms, manual
+ declarations might have to be added to the target context of the
+ interpretation to revert such declarations.
\end{warn}
\begin{warn}
--- a/doc-src/Locales/Locales/Examples3.thy Tue Nov 24 10:33:02 2009 +0100
+++ b/doc-src/Locales/Locales/Examples3.thy Tue Nov 24 10:33:21 2009 +0100
@@ -591,7 +591,7 @@
( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\
\textit{instance} & ::=
& [ \textit{qualifier} ``\textbf{:}'' ]
- \textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
+ \textit{name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
\textit{expression} & ::=
& \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$
[ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex]
@@ -625,8 +625,8 @@
\textit{toplevel} & ::=
& \textbf{print\_locales} \\
- & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\
- & | & \textbf{print\_interps} \textit{locale}
+ & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{name} \\
+ & | & \textbf{print\_interps} \textit{name}
\end{tabular}
\end{center}
\hrule
--- a/doc-src/Locales/Locales/document/Examples3.tex Tue Nov 24 10:33:02 2009 +0100
+++ b/doc-src/Locales/Locales/document/Examples3.tex Tue Nov 24 10:33:21 2009 +0100
@@ -882,7 +882,7 @@
( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\
\textit{instance} & ::=
& [ \textit{qualifier} ``\textbf{:}'' ]
- \textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
+ \textit{name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
\textit{expression} & ::=
& \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$
[ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex]
@@ -916,8 +916,8 @@
\textit{toplevel} & ::=
& \textbf{print\_locales} \\
- & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\
- & | & \textbf{print\_interps} \textit{locale}
+ & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{name} \\
+ & | & \textbf{print\_interps} \textit{name}
\end{tabular}
\end{center}
\hrule
--- a/etc/isar-keywords-ZF.el Tue Nov 24 10:33:02 2009 +0100
+++ b/etc/isar-keywords-ZF.el Tue Nov 24 10:33:21 2009 +0100
@@ -19,6 +19,7 @@
"ProofGeneral\\.inform_file_processed"
"ProofGeneral\\.inform_file_retracted"
"ProofGeneral\\.kill_proof"
+ "ProofGeneral\\.pr"
"ProofGeneral\\.process_pgip"
"ProofGeneral\\.restart"
"ProofGeneral\\.undo"
@@ -271,6 +272,7 @@
(defconst isar-keywords-diag
'("ML_command"
"ML_val"
+ "ProofGeneral\\.pr"
"cd"
"class_deps"
"commit"
--- a/etc/isar-keywords.el Tue Nov 24 10:33:02 2009 +0100
+++ b/etc/isar-keywords.el Tue Nov 24 10:33:21 2009 +0100
@@ -19,6 +19,7 @@
"ProofGeneral\\.inform_file_processed"
"ProofGeneral\\.inform_file_retracted"
"ProofGeneral\\.kill_proof"
+ "ProofGeneral\\.pr"
"ProofGeneral\\.process_pgip"
"ProofGeneral\\.restart"
"ProofGeneral\\.undo"
@@ -345,6 +346,7 @@
(defconst isar-keywords-diag
'("ML_command"
"ML_val"
+ "ProofGeneral\\.pr"
"atp_info"
"atp_kill"
"atp_messages"
--- a/src/HOL/Library/Transitive_Closure_Table.thy Tue Nov 24 10:33:02 2009 +0100
+++ b/src/HOL/Library/Transitive_Closure_Table.thy Tue Nov 24 10:33:21 2009 +0100
@@ -185,7 +185,7 @@
by (auto simp add: rtranclp_eq_rtrancl_path)
qed
-declare rtranclp_eq_rtrancl_tab_nil [code_unfold]
+declare rtranclp_eq_rtrancl_tab_nil [code_unfold, code_inline del]
declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro]
@@ -224,7 +224,11 @@
values "{x. test\<^sup>*\<^sup>* A x}"
values "{x. test\<^sup>*\<^sup>* x C}"
-hide const test
+value "test\<^sup>*\<^sup>* A C"
+value "test\<^sup>*\<^sup>* C A"
+
+hide type ty
+hide const test A B C
end
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Nov 24 10:33:02 2009 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Nov 24 10:33:21 2009 +0100
@@ -190,6 +190,12 @@
local structure P = OuterParse and K = OuterKeyword in
+fun prP () =
+ OuterSyntax.improper_command "ProofGeneral.pr" "print state (internal)" K.diag
+ (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
+ if Toplevel.is_toplevel state orelse Toplevel.is_theory state then tell_clear_goals ()
+ else (Toplevel.quiet := false; Toplevel.print_state true state))));
+
fun undoP () = (*undo without output -- historical*)
OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)));
@@ -219,7 +225,8 @@
(fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt))));
fun init_outer_syntax () = List.app (fn f => f ())
- [undoP, restartP, kill_proofP, inform_file_processedP, inform_file_retractedP, process_pgipP];
+ [prP, undoP, restartP, kill_proofP, inform_file_processedP,
+ inform_file_retractedP, process_pgipP];
end;