--- a/ANNOUNCE Thu Apr 16 10:11:35 2009 +0200
+++ b/ANNOUNCE Thu Apr 16 10:11:45 2009 +0200
@@ -25,8 +25,7 @@
* Simplified arrangement of Isabelle startup scripts and settings
directory.
-* Simplified internal programming interfaces for all Isar language
-elements.
+* Simplified programming interfaces for all Isar language elements.
* General high-level support for concurrent ML programming.
--- a/INSTALL Thu Apr 16 10:11:35 2009 +0200
+++ b/INSTALL Thu Apr 16 10:11:45 2009 +0200
@@ -6,7 +6,7 @@
----------------------
The Isabelle distribution includes both complete sources and
-precompiled binary packages for common Unix platforms.
+precompiled binary packages for common Unix-like platforms.
Quick installation
--- a/README Thu Apr 16 10:11:35 2009 +0200
+++ b/README Thu Apr 16 10:11:45 2009 +0200
@@ -14,7 +14,7 @@
* A full Standard ML Compiler (works best with Poly/ML 5.2.1).
* The GNU bash shell (version 3.x or 2.x).
* Perl (version 5.x).
- * GNU Emacs (version 21, 22) or XEmacs (version 21.4.x)
+ * GNU Emacs (version 21, 22, 23) or XEmacs (version 21.4.x)
-- for the Proof General interface.
* A complete LaTeX installation -- for document preparation.
@@ -22,9 +22,8 @@
Binary packages are available for Isabelle/HOL and ZF for several
platforms from the Isabelle web page. The system may be easily
- built from scratch as well, taking the traditional tar.gz source
- distribution. See file INSTALL as distributed with Isabelle for
- more information.
+ built from scratch, using the tar.gz source distribution. See file
+ INSTALL as distributed with Isabelle for more information.
Further background information may be found in the Isabelle System
Manual, distributed with the sources (directory doc).
@@ -36,8 +35,8 @@
including Isabelle. Proof General is suitable for use by pacifists
and Emacs militants alike. Its most prominent feature is script
management, providing a metaphor of live proof script editing.
- Proof General also provides some support for proper mathematical
- symbols displayed on screen.
+ Proof General also provides some support for mathematical symbols
+ displayed on screen.
Other sources of information
--- a/src/HOL/Tools/atp_wrapper.ML Thu Apr 16 10:11:35 2009 +0200
+++ b/src/HOL/Tools/atp_wrapper.ML Thu Apr 16 10:11:45 2009 +0200
@@ -79,14 +79,16 @@
val failure = find_failure proof
val success = rc = 0 andalso is_none failure
val message =
- if isSome failure then "Proof attempt failed."
- else if rc <> 0 then "Proof attempt failed: " ^ proof
+ if is_some failure then "External prover failed."
+ else if rc <> 0 then "External prover failed: " ^ proof
else "Try this command: " ^ produce_answer (proof, thm_names, ctxt, th, subgoalno)
- val _ = if isSome failure
+ val _ =
+ if is_some failure
then Output.debug (fn () => "Sledgehammer failure: " ^ the failure ^ "\nOutput: " ^ proof)
else ()
- val _ = if rc <> 0
+ val _ =
+ if rc <> 0
then Output.debug (fn () => "Sledgehammer exited with return code " ^ string_of_int rc ^ ":\n" ^ proof)
else ()
in (success, message) end;