# HG changeset patch
# User haftmann
# Date 1239869505 -7200
# Node ID 0d126d4a3b0f4c07dcc5b386b7888e86ecf3f299
# Parent  35f255987e18624428ac786606bd85ef4256832b# Parent  16912b4e66252eaa76523c5caf6f65dcba632741
merged

diff -r 35f255987e18 -r 0d126d4a3b0f ANNOUNCE
--- 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.
 
diff -r 35f255987e18 -r 0d126d4a3b0f INSTALL
--- 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
diff -r 35f255987e18 -r 0d126d4a3b0f README
--- 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
 
diff -r 35f255987e18 -r 0d126d4a3b0f src/HOL/Tools/atp_wrapper.ML
--- 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;