1.1 --- a/ANNOUNCE Tue Nov 24 10:33:02 2009 +0100
1.2 +++ b/ANNOUNCE Tue Nov 24 10:33:21 2009 +0100
1.3 @@ -7,7 +7,34 @@
1.4 file in the distribution for more details. Some important changes
1.5 are:
1.6
1.7 -* FIXME
1.8 +* Isabelle tool "wwwfind" provides web interface for 'find_theorems'
1.9 +on a given logic image.
1.10 +
1.11 +* HOL-SMT: proof method "smt" for a combination of first-order logic
1.12 +with equality, linear and nonlinear (natural/integer/real) arithmetic,
1.13 +and fixed-size bitvectors.
1.14 +
1.15 +* HOL-Boogie: an interactive prover back-end for Boogie and VCC.
1.16 +
1.17 +* HOL: Counterexample generator tool Nitpick based on the Kodkod
1.18 +relational model finder.
1.19 +
1.20 +* HOL: predicate compiler turning inductive into (executable)
1.21 +equational specifications.
1.22 +
1.23 +* HOL: refined number theory.
1.24 +
1.25 +* HOL: various parts of multivariate analysis.
1.26 +
1.27 +* HOLCF: new definitional domain package.
1.28 +
1.29 +* Revised tutorial on locales.
1.30 +
1.31 +* Support for Poly/ML 5.3.0, with improved reporting of compiler
1.32 +errors and run-time exceptions, including detailed source positions.
1.33 +
1.34 +* Parallel checking of nested Isar proofs, with improved scalability
1.35 +up to 8 cores.
1.36
1.37
1.38 You may get Isabelle2009-1 from the following mirror sites:
2.1 --- a/Admin/E/README Tue Nov 24 10:33:02 2009 +0100
2.2 +++ b/Admin/E/README Tue Nov 24 10:33:21 2009 +0100
2.3 @@ -1,4 +1,3 @@
2.4 -
2.5 This distribution of E 1.0-004 has been compiled according to the
2.6 README included in the official version from
2.7 http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html
2.8 @@ -8,23 +7,12 @@
2.9 $ ./configure
2.10 $ make
2.11
2.12 -The resulting PROVER/eproof executable has been changed to be
2.13 -relocatable:
2.14 -
2.15 - $ diff eproof-orig eproof
2.16 - 1c1
2.17 - < #!/bin/bash -f
2.18 - ---
2.19 - > #!/usr/bin/env bash
2.20 - 3c3,4
2.21 - < EXECPATH=/Users/schulz/SOURCES/Projects/E/PROVER
2.22 - ---
2.23 - > set -o noglob
2.24 - > EXECPATH="$(cd "$(dirname "$0")"; pwd)"
2.25 +The PROVER/eproof executable has been replaced by a version written in
2.26 +perl (by Sascha Boehme).
2.27
2.28 Now the main executables in PROVER/ are moved to the platform-specific
2.29 target directory (E/x86-linux etc.).
2.30
2.31
2.32 - Makarius
2.33 - 07-Apr-2009
2.34 + Makarius
2.35 + 23-Nov-2009
3.1 --- a/INSTALL Tue Nov 24 10:33:02 2009 +0100
3.2 +++ b/INSTALL Tue Nov 24 10:33:21 2009 +0100
3.3 @@ -17,7 +17,7 @@
3.4 site installation of Isabelle on Linux/x86 works like this:
3.5
3.6 tar -C /usr/local -xzf Isabelle.tar.gz
3.7 - tar -C /usr/local -xzf polyml_x86-linux.tar.gz
3.8 + tar -C /usr/local -xzf polyml.tar.gz
3.9 tar -C /usr/local -xzf HOL_x86-linux.tar.gz
3.10
3.11 The install prefix given above may be changed as appropriate; there is
4.1 --- a/NEWS Tue Nov 24 10:33:02 2009 +0100
4.2 +++ b/NEWS Tue Nov 24 10:33:21 2009 +0100
4.3 @@ -114,19 +114,17 @@
4.4 fixpoint theorem.
4.5
4.6 * Reorganization of number theory, INCOMPATIBILITY:
4.7 - - new number theory development for nat and int, in
4.8 - theories Divides and GCD as well as in new session
4.9 - Number_Theory
4.10 - - some constants and facts now suffixed with _nat and
4.11 - _int accordingly
4.12 - - former session NumberTheory now named Old_Number_Theory,
4.13 - including theories Legacy_GCD and Primes (prefer Number_Theory
4.14 - if possible)
4.15 + - new number theory development for nat and int, in theories Divides
4.16 + and GCD as well as in new session Number_Theory
4.17 + - some constants and facts now suffixed with _nat and _int
4.18 + accordingly
4.19 + - former session NumberTheory now named Old_Number_Theory, including
4.20 + theories Legacy_GCD and Primes (prefer Number_Theory if possible)
4.21 - moved theory Pocklington from src/HOL/Library to
4.22 src/HOL/Old_Number_Theory
4.23
4.24 -* Theory GCD includes functions Gcd/GCD and Lcm/LCM for the gcd and lcm
4.25 -of finite and infinite sets. It is shown that they form a complete
4.26 +* Theory GCD includes functions Gcd/GCD and Lcm/LCM for the gcd and
4.27 +lcm of finite and infinite sets. It is shown that they form a complete
4.28 lattice.
4.29
4.30 * Class semiring_div requires superclass no_zero_divisors and proof of
4.31 @@ -198,8 +196,6 @@
4.32 abbreviation for "inv_into UNIV". Lemmas are renamed accordingly.
4.33 INCOMPATIBILITY.
4.34
4.35 ---
4.36 -
4.37 * Most rules produced by inductive and datatype package have mandatory
4.38 prefixes. INCOMPATIBILITY.
4.39
4.40 @@ -208,8 +204,9 @@
4.41 DERIV_intros assumes composition with an additional function and
4.42 matches a variable to the derivative, which has to be solved by the
4.43 Simplifier. Hence (auto intro!: DERIV_intros) computes the derivative
4.44 -of most elementary terms. Former Maclauren.DERIV_tac and Maclauren.deriv_tac
4.45 -should be replaced by (auto intro!: DERIV_intros). INCOMPATIBILITY.
4.46 +of most elementary terms. Former Maclauren.DERIV_tac and
4.47 +Maclauren.deriv_tac should be replaced by (auto intro!: DERIV_intros).
4.48 +INCOMPATIBILITY.
4.49
4.50 * Code generator attributes follow the usual underscore convention:
4.51 code_unfold replaces code unfold
4.52 @@ -274,7 +271,8 @@
4.53 * The 'fixrec' package now supports "bottom patterns". Bottom
4.54 patterns can be used to generate strictness rules, or to make
4.55 functions more strict (much like the bang-patterns supported by the
4.56 -Glasgow Haskell Compiler). See src/HOLCF/ex/Fixrec_ex.thy for examples.
4.57 +Glasgow Haskell Compiler). See src/HOLCF/ex/Fixrec_ex.thy for
4.58 +examples.
4.59
4.60
4.61 *** ML ***
5.1 --- a/doc-src/IsarRef/Thy/Spec.thy Tue Nov 24 10:33:02 2009 +0100
5.2 +++ b/doc-src/IsarRef/Thy/Spec.thy Tue Nov 24 10:33:21 2009 +0100
5.3 @@ -456,13 +456,10 @@
5.4 \secref{sec:object-logic}). Separate introduction rules @{text
5.5 loc_axioms.intro} and @{text loc.intro} are provided as well.
5.6
5.7 - \item @{command "print_locale"}~@{text "import + body"} prints the
5.8 - specified locale expression in a flattened form. The notable
5.9 - special case @{command "print_locale"}~@{text loc} just prints the
5.10 - contents of the named locale, but keep in mind that type-inference
5.11 - will normalize type variables according to the usual alphabetical
5.12 - order. The command omits @{element "notes"} elements by default.
5.13 - Use @{command "print_locale"}@{text "!"} to get them included.
5.14 + \item @{command "print_locale"}~@{text "locale"} prints the
5.15 + contents of the named locale. The command omits @{element "notes"}
5.16 + elements by default. Use @{command "print_locale"}@{text "!"} to
5.17 + have them included.
5.18
5.19 \item @{command "print_locales"} prints the names of all locales
5.20 of the current theory.
5.21 @@ -537,7 +534,7 @@
5.22 qualifier, although only for fragments of @{text expr} that are not
5.23 interpreted in the theory already.
5.24
5.25 - \item @{command "interpretation"}~@{text "expr insts \<WHERE> eqns"}
5.26 + \item @{command "interpretation"}~@{text "expr \<WHERE> eqns"}
5.27 interprets @{text expr} in the theory. The command generates proof
5.28 obligations for the instantiated specifications (assumes and defines
5.29 elements). Once these are discharged by the user, instantiated
5.30 @@ -563,19 +560,24 @@
5.31 interpretations dynamically participate in any facts added to
5.32 locales.
5.33
5.34 - \item @{command "interpret"}~@{text "expr insts"}
5.35 + \item @{command "interpret"}~@{text "expr"}
5.36 interprets @{text expr} in the proof context and is otherwise
5.37 similar to interpretation in theories.
5.38
5.39 + \item @{command "print_interps"}~@{text "locale"} lists all
5.40 + interpretations of @{text "locale"} in the current theory, including
5.41 + those due to a combination of an @{command "interpretation"} and
5.42 + one or several @{command "sublocale"} declarations.
5.43 +
5.44 \end{description}
5.45
5.46 \begin{warn}
5.47 Since attributes are applied to interpreted theorems,
5.48 interpretation may modify the context of common proof tools, e.g.\
5.49 - the Simplifier or Classical Reasoner. Since the behavior of such
5.50 - automated reasoning tools is \emph{not} stable under
5.51 - interpretation morphisms, manual declarations might have to be
5.52 - added to revert such declarations.
5.53 + the Simplifier or Classical Reasoner. As the behavior of such
5.54 + tools is \emph{not} stable under interpretation morphisms, manual
5.55 + declarations might have to be added to the target context of the
5.56 + interpretation to revert such declarations.
5.57 \end{warn}
5.58
5.59 \begin{warn}
6.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex Tue Nov 24 10:33:02 2009 +0100
6.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Tue Nov 24 10:33:21 2009 +0100
6.3 @@ -478,13 +478,10 @@
6.4 \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} by \isa{{\isachardoublequote}{\isasymlongrightarrow}{\isachardoublequote}} in HOL; see also
6.5 \secref{sec:object-logic}). Separate introduction rules \isa{loc{\isacharunderscore}axioms{\isachardot}intro} and \isa{loc{\isachardot}intro} are provided as well.
6.6
6.7 - \item \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}import\ {\isacharplus}\ body{\isachardoublequote}} prints the
6.8 - specified locale expression in a flattened form. The notable
6.9 - special case \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{loc} just prints the
6.10 - contents of the named locale, but keep in mind that type-inference
6.11 - will normalize type variables according to the usual alphabetical
6.12 - order. The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}} elements by default.
6.13 - Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to get them included.
6.14 + \item \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}locale{\isachardoublequote}} prints the
6.15 + contents of the named locale. The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}}
6.16 + elements by default. Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to
6.17 + have them included.
6.18
6.19 \item \hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}} prints the names of all locales
6.20 of the current theory.
6.21 @@ -559,7 +556,7 @@
6.22 qualifier, although only for fragments of \isa{expr} that are not
6.23 interpreted in the theory already.
6.24
6.25 - \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}
6.26 + \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ {\isasymWHERE}\ eqns{\isachardoublequote}}
6.27 interprets \isa{expr} in the theory. The command generates proof
6.28 obligations for the instantiated specifications (assumes and defines
6.29 elements). Once these are discharged by the user, instantiated
6.30 @@ -585,19 +582,24 @@
6.31 interpretations dynamically participate in any facts added to
6.32 locales.
6.33
6.34 - \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr\ insts{\isachardoublequote}}
6.35 + \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr{\isachardoublequote}}
6.36 interprets \isa{expr} in the proof context and is otherwise
6.37 similar to interpretation in theories.
6.38
6.39 + \item \hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}~\isa{{\isachardoublequote}locale{\isachardoublequote}} lists all
6.40 + interpretations of \isa{{\isachardoublequote}locale{\isachardoublequote}} in the current theory, including
6.41 + those due to a combination of an \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} and
6.42 + one or several \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}} declarations.
6.43 +
6.44 \end{description}
6.45
6.46 \begin{warn}
6.47 Since attributes are applied to interpreted theorems,
6.48 interpretation may modify the context of common proof tools, e.g.\
6.49 - the Simplifier or Classical Reasoner. Since the behavior of such
6.50 - automated reasoning tools is \emph{not} stable under
6.51 - interpretation morphisms, manual declarations might have to be
6.52 - added to revert such declarations.
6.53 + the Simplifier or Classical Reasoner. As the behavior of such
6.54 + tools is \emph{not} stable under interpretation morphisms, manual
6.55 + declarations might have to be added to the target context of the
6.56 + interpretation to revert such declarations.
6.57 \end{warn}
6.58
6.59 \begin{warn}
7.1 --- a/doc-src/Locales/Locales/Examples3.thy Tue Nov 24 10:33:02 2009 +0100
7.2 +++ b/doc-src/Locales/Locales/Examples3.thy Tue Nov 24 10:33:21 2009 +0100
7.3 @@ -591,7 +591,7 @@
7.4 ( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\
7.5 \textit{instance} & ::=
7.6 & [ \textit{qualifier} ``\textbf{:}'' ]
7.7 - \textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
7.8 + \textit{name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
7.9 \textit{expression} & ::=
7.10 & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$
7.11 [ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex]
7.12 @@ -625,8 +625,8 @@
7.13
7.14 \textit{toplevel} & ::=
7.15 & \textbf{print\_locales} \\
7.16 - & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\
7.17 - & | & \textbf{print\_interps} \textit{locale}
7.18 + & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{name} \\
7.19 + & | & \textbf{print\_interps} \textit{name}
7.20 \end{tabular}
7.21 \end{center}
7.22 \hrule
8.1 --- a/doc-src/Locales/Locales/document/Examples3.tex Tue Nov 24 10:33:02 2009 +0100
8.2 +++ b/doc-src/Locales/Locales/document/Examples3.tex Tue Nov 24 10:33:21 2009 +0100
8.3 @@ -882,7 +882,7 @@
8.4 ( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\
8.5 \textit{instance} & ::=
8.6 & [ \textit{qualifier} ``\textbf{:}'' ]
8.7 - \textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
8.8 + \textit{name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
8.9 \textit{expression} & ::=
8.10 & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$
8.11 [ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex]
8.12 @@ -916,8 +916,8 @@
8.13
8.14 \textit{toplevel} & ::=
8.15 & \textbf{print\_locales} \\
8.16 - & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\
8.17 - & | & \textbf{print\_interps} \textit{locale}
8.18 + & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{name} \\
8.19 + & | & \textbf{print\_interps} \textit{name}
8.20 \end{tabular}
8.21 \end{center}
8.22 \hrule
9.1 --- a/etc/isar-keywords-ZF.el Tue Nov 24 10:33:02 2009 +0100
9.2 +++ b/etc/isar-keywords-ZF.el Tue Nov 24 10:33:21 2009 +0100
9.3 @@ -19,6 +19,7 @@
9.4 "ProofGeneral\\.inform_file_processed"
9.5 "ProofGeneral\\.inform_file_retracted"
9.6 "ProofGeneral\\.kill_proof"
9.7 + "ProofGeneral\\.pr"
9.8 "ProofGeneral\\.process_pgip"
9.9 "ProofGeneral\\.restart"
9.10 "ProofGeneral\\.undo"
9.11 @@ -271,6 +272,7 @@
9.12 (defconst isar-keywords-diag
9.13 '("ML_command"
9.14 "ML_val"
9.15 + "ProofGeneral\\.pr"
9.16 "cd"
9.17 "class_deps"
9.18 "commit"
10.1 --- a/etc/isar-keywords.el Tue Nov 24 10:33:02 2009 +0100
10.2 +++ b/etc/isar-keywords.el Tue Nov 24 10:33:21 2009 +0100
10.3 @@ -19,6 +19,7 @@
10.4 "ProofGeneral\\.inform_file_processed"
10.5 "ProofGeneral\\.inform_file_retracted"
10.6 "ProofGeneral\\.kill_proof"
10.7 + "ProofGeneral\\.pr"
10.8 "ProofGeneral\\.process_pgip"
10.9 "ProofGeneral\\.restart"
10.10 "ProofGeneral\\.undo"
10.11 @@ -345,6 +346,7 @@
10.12 (defconst isar-keywords-diag
10.13 '("ML_command"
10.14 "ML_val"
10.15 + "ProofGeneral\\.pr"
10.16 "atp_info"
10.17 "atp_kill"
10.18 "atp_messages"
11.1 --- a/src/HOL/Library/Transitive_Closure_Table.thy Tue Nov 24 10:33:02 2009 +0100
11.2 +++ b/src/HOL/Library/Transitive_Closure_Table.thy Tue Nov 24 10:33:21 2009 +0100
11.3 @@ -185,7 +185,7 @@
11.4 by (auto simp add: rtranclp_eq_rtrancl_path)
11.5 qed
11.6
11.7 -declare rtranclp_eq_rtrancl_tab_nil [code_unfold]
11.8 +declare rtranclp_eq_rtrancl_tab_nil [code_unfold, code_inline del]
11.9
11.10 declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro]
11.11
11.12 @@ -224,7 +224,11 @@
11.13 values "{x. test\<^sup>*\<^sup>* A x}"
11.14 values "{x. test\<^sup>*\<^sup>* x C}"
11.15
11.16 -hide const test
11.17 +value "test\<^sup>*\<^sup>* A C"
11.18 +value "test\<^sup>*\<^sup>* C A"
11.19 +
11.20 +hide type ty
11.21 +hide const test A B C
11.22
11.23 end
11.24
12.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Nov 24 10:33:02 2009 +0100
12.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Nov 24 10:33:21 2009 +0100
12.3 @@ -190,6 +190,12 @@
12.4
12.5 local structure P = OuterParse and K = OuterKeyword in
12.6
12.7 +fun prP () =
12.8 + OuterSyntax.improper_command "ProofGeneral.pr" "print state (internal)" K.diag
12.9 + (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
12.10 + if Toplevel.is_toplevel state orelse Toplevel.is_theory state then tell_clear_goals ()
12.11 + else (Toplevel.quiet := false; Toplevel.print_state true state))));
12.12 +
12.13 fun undoP () = (*undo without output -- historical*)
12.14 OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
12.15 (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)));
12.16 @@ -219,7 +225,8 @@
12.17 (fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt))));
12.18
12.19 fun init_outer_syntax () = List.app (fn f => f ())
12.20 - [undoP, restartP, kill_proofP, inform_file_processedP, inform_file_retractedP, process_pgipP];
12.21 + [prP, undoP, restartP, kill_proofP, inform_file_processedP,
12.22 + inform_file_retractedP, process_pgipP];
12.23
12.24 end;
12.25