# HG changeset patch
# User huffman
# Date 1240321454 25200
# Node ID 182fa14e1844ad7e472d0dbb1de489a5159076f9
# Parent  e3bbc2c4c58147226bf6360423b0b3cd60179cae# Parent  a3d2128cac92bc2fe013023627aab2ac88d80b26
merged

diff -r a3d2128cac92 -r 182fa14e1844 .hgtags
--- a/.hgtags	Mon Apr 20 17:38:25 2009 -0700
+++ b/.hgtags	Tue Apr 21 06:44:14 2009 -0700
@@ -23,5 +23,4 @@
 dde117622dace696123b023d1f06cf8d8ef9eb46 nominal_02
 f9eb0f819642b2ad77119dbf8935bf13248f205d Isabelle94
 fc385ce6187d5ad2cef90f1e6240cc691e02d827 Isabelle2005
-613c2eb8aef60d016a427011bd8236519b22209a isa2009-test
-dda08b76fa999333af77a2afa08aef09cbcd34d2 isa2009-test
+5c8618f95d240046bbbb609b643c06704888f587 Isabelle2009
diff -r a3d2128cac92 -r 182fa14e1844 ANNOUNCE
--- a/ANNOUNCE	Mon Apr 20 17:38:25 2009 -0700
+++ b/ANNOUNCE	Tue Apr 21 06:44:14 2009 -0700
@@ -8,7 +8,7 @@
 are:
 
 * Complete re-implementation of locales, with proper support for local
-syntax, and more robust interpretation mechanism.
+syntax, and more general locale expressions.
 
 * New 'find_consts' and 'find_theorems' facilities, together with
 "auto solve" feature of toplevel goal statements.
@@ -25,13 +25,14 @@
 * 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.
 
 * Parallel proof checking within Isar theories.
 
+* Haskabelle importer from Haskell source files to Isar theories.
+
 
 You may get Isabelle2009 from the following mirror sites:
 
diff -r a3d2128cac92 -r 182fa14e1844 Admin/CHECKLIST
--- a/Admin/CHECKLIST	Mon Apr 20 17:38:25 2009 -0700
+++ b/Admin/CHECKLIST	Tue Apr 21 06:44:14 2009 -0700
@@ -1,10 +1,13 @@
 Checklist for official releases
 ===============================
 
-- test mosml, polyml-5.0, polyml-4.1.3, polyml-4.1.4, polyml-4.2.0, x86-solaris, x86-cygwin;
+- test mosml, polyml-5.2, polyml-5.1, polyml-5.0, polyml-4.1.3, polyml-4.1.4, polyml-4.2.0,
+  sparc-solaris, x86-solaris;
 
 - test ProofGeneral;
 
+- test Scala wrapper;
+
 - check HTML header of library;
 
 - check CTRL-C, SIGINT in tty (also for external processes);
@@ -13,7 +16,9 @@
 
 - Admin/update-keywords;
 
-- check ANNOUNCE, README, INSTALL, NEWS, COPYRIGHT, CONTRIBUTORS, ~isabelle/website;
+- check ANNOUNCE, README, INSTALL, NEWS, COPYRIGHT, CONTRIBUTORS;
+
+- update https://isabelle.in.tum.de/repos/website;
 
 - maintain Docs:
     doc-src/Dirs
@@ -24,6 +29,3 @@
     lib/Tools/makeall
     lib/html/library_index_content.template
 
-- after release: 
-    commit new ~isabelle/website/include/documentationdist.include.html to website SVN
-
diff -r a3d2128cac92 -r 182fa14e1844 Admin/MacOS/README
--- a/Admin/MacOS/README	Mon Apr 20 17:38:25 2009 -0700
+++ b/Admin/MacOS/README	Tue Apr 21 06:44:14 2009 -0700
@@ -3,15 +3,7 @@
 
 Requirements:
 
-* CocoaDialog http://cocoadialog.sourceforge.net/
-
-* Platypus http://www.sveinbjorn.org/platypus
-
-* AppHack 1.1 http://www.sveinbjorn.org/apphack
+* CocoaDialog 2.2.1 http://cocoadialog.sourceforge.net/
 
-  Manual setup:
-    File type: "Isabelle theory"
-    Icon: "theory.icns"
-    "Editor"
-    Suffixes: "thy"
+* Platypus 4.0 http://www.sveinbjorn.org/platypus
 
diff -r a3d2128cac92 -r 182fa14e1844 Admin/MacOS/mk
--- a/Admin/MacOS/mk	Mon Apr 20 17:38:25 2009 -0700
+++ b/Admin/MacOS/mk	Tue Apr 21 06:44:14 2009 -0700
@@ -11,7 +11,6 @@
   -a Isabelle -u Isabelle \
   -I "de.tum.in.isabelle" \
   -i "$THIS/isabelle.icns" \
-  -D -X thy \
   -p /bin/bash \
   -c "$THIS/script" \
   -o None \
diff -r a3d2128cac92 -r 182fa14e1844 Admin/MacOS/script
--- a/Admin/MacOS/script	Mon Apr 20 17:38:25 2009 -0700
+++ b/Admin/MacOS/script	Tue Apr 21 06:44:14 2009 -0700
@@ -49,7 +49,7 @@
   "")"
 
 if [ -n "$PROOFGENERAL_EMACS" ]; then
-  PROOFGENERAL_OPTIONS="-p $PROOFGENERAL_EMACS $PROOFGENERAL_OPTIONS"
+  EMACS_OPTIONS="-p $PROOFGENERAL_EMACS"
 fi
 
 
@@ -57,7 +57,7 @@
 
 OUTPUT="/tmp/isabelle$$.out"
 
-( "$HOME/bin/isabelle" emacs "$@" ) > "$OUTPUT" 2>&1
+( "$ISABELLE_TOOL" emacs $EMACS_OPTIONS "$@" ) > "$OUTPUT" 2>&1
 RC=$?
 
 if [ "$RC" != 0 ]; then
diff -r a3d2128cac92 -r 182fa14e1844 COPYRIGHT
--- a/COPYRIGHT	Mon Apr 20 17:38:25 2009 -0700
+++ b/COPYRIGHT	Tue Apr 21 06:44:14 2009 -0700
@@ -1,6 +1,6 @@
 ISABELLE COPYRIGHT NOTICE, LICENCE AND DISCLAIMER.
 
-Copyright (c) 2008,
+Copyright (c) 2009,
   University of Cambridge and
   Technische Universitaet Muenchen.
 
diff -r a3d2128cac92 -r 182fa14e1844 INSTALL
--- a/INSTALL	Mon Apr 20 17:38:25 2009 -0700
+++ b/INSTALL	Tue Apr 21 06:44:14 2009 -0700
@@ -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 a3d2128cac92 -r 182fa14e1844 NEWS
--- a/NEWS	Mon Apr 20 17:38:25 2009 -0700
+++ b/NEWS	Tue Apr 21 06:44:14 2009 -0700
@@ -1,6 +1,11 @@
 Isabelle NEWS -- history user-relevant changes
 ==============================================
 
+New in this Isabelle version
+----------------------------
+
+
+
 New in Isabelle2009 (April 2009)
 --------------------------------
 
diff -r a3d2128cac92 -r 182fa14e1844 README
--- a/README	Mon Apr 20 17:38:25 2009 -0700
+++ b/README	Tue Apr 21 06:44:14 2009 -0700
@@ -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 a3d2128cac92 -r 182fa14e1844 etc/settings
--- a/etc/settings	Mon Apr 20 17:38:25 2009 -0700
+++ b/etc/settings	Tue Apr 21 06:44:14 2009 -0700
@@ -90,7 +90,8 @@
 ### Batch sessions (cf. isabelle usedir)
 ###
 
-ISABELLE_USEDIR_OPTIONS="-M max -p 1 -v true -V outline=/proof,/ML"
+ISABELLE_USEDIR_OPTIONS="-M 1 -p 1 -v true -V outline=/proof,/ML"
+#ISABELLE_USEDIR_OPTIONS="-M max -p 1 -v true -V outline=/proof,/ML"
 
 # Specifically for the HOL image
 HOL_USEDIR_OPTIONS=""
diff -r a3d2128cac92 -r 182fa14e1844 src/HOL/Tools/atp_wrapper.ML
--- a/src/HOL/Tools/atp_wrapper.ML	Mon Apr 20 17:38:25 2009 -0700
+++ b/src/HOL/Tools/atp_wrapper.ML	Tue Apr 21 06:44:14 2009 -0700
@@ -68,7 +68,7 @@
     val fname = File.platform_path probfile
     val thm_names = write_problem_file probfile th subgoalno axiom_clauses thy
     val cmdline =
-      if File.exists cmd then File.shell_path cmd ^ " " ^ args
+      if File.exists cmd then "exec " ^ File.shell_path cmd ^ " " ^ args
       else error ("Bad executable: " ^ Path.implode cmd)
     val (proof, rc) = system_out (cmdline ^ " " ^ fname)
 
@@ -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;