# HG changeset patch
# User wenzelm
# Date 1337767347 -7200
# Node ID c5f7be4a1734b7d8c1d322a64c09b2ed4b9fb99f
# Parent  d2bdd85ee23c6639f969cacc50b1fb34c9da6725# Parent  7d30534e545bc1bcabee753b58f5721159520fb4
merged, abandoning change of src/HOL/Tools/ATP/atp_problem_generate.ML from 6ea205a4d7fd;

diff -r d2bdd85ee23c -r c5f7be4a1734 .hgtags
--- a/.hgtags	Tue May 22 16:59:27 2012 +0200
+++ b/.hgtags	Wed May 23 12:02:27 2012 +0200
@@ -28,4 +28,4 @@
 35815ce9218a8822a50f5d80b96aa8d1970ec35d Isabelle2009-2
 6d736d983d5cfec4a6c6fba174db2cd93493a96b Isabelle2011
 76fef3e570043b84a32716b5633085d2fb215525 Isabelle2011-1
-
+21c42b095c841d1a7508c143d6b6e98d95dbfa69 Isabelle2012
diff -r d2bdd85ee23c -r c5f7be4a1734 ANNOUNCE
--- a/ANNOUNCE	Tue May 22 16:59:27 2012 +0200
+++ b/ANNOUNCE	Wed May 23 12:02:27 2012 +0200
@@ -3,10 +3,35 @@
 
 Isabelle2012 is now available.
 
-This version significantly improves upon Isabelle2011-1, see the NEWS
-file in the distribution for more details.  Some notable changes are:
+This version introduces many changes and improvements over
+Isabelle2011-1, see the NEWS file in the distribution for more
+details.  Some highlights are:
+
+* Improved Isabelle/jEdit Prover IDE (PIDE).
+
+* Support for block-structured specification contexts.
+
+* Discontinued old code generator.
+
+* Updated manuals: prog-prove, isar-ref, implementation, system.
+
+* HOL: type 'a set is proper type constructor again.
 
-* FIXME
+* HOL: improved representation of numerals.
+
+* HOL: new transfer and lifting packages, improved quotient package.
+
+* HOL tool enhancements: Quickcheck, Nitpick, Sledgehammer.
+
+* HOL library enhancements, including HOL-Library and HOL-Probability.
+
+* HOL: more TPTP support.
+
+* Re-implementation of HOL-Import for HOL-Light.
+
+* ZF: some modernization of notation and proofs.
+
+* System integration: improved support of Windows platform.
 
 
 You may get Isabelle2012 from the following mirror sites:
diff -r d2bdd85ee23c -r c5f7be4a1734 Admin/CHECKLIST
--- a/Admin/CHECKLIST	Tue May 22 16:59:27 2012 +0200
+++ b/Admin/CHECKLIST	Wed May 23 12:02:27 2012 +0200
@@ -67,10 +67,9 @@
 
 - makedist: REPOS_NAME="isabelle-release"
 
-- hgrc: default = /home/isabelle-repository/repos/isabelle-release
+- various .hg/hgrc files:
+  default = /home/isabelle-repository/repos/isabelle-release
 
-  isatest@macbroy28:hg-isabelle/.hg/hgrc
-  isatest@atbroy102:hg-isabelle/.hg/hgrc
-
+- isatest@macbroy28:hg-isabelle/.hg/hgrc
 - isatest@macbroy28:devel-page/content/index.content
 
diff -r d2bdd85ee23c -r c5f7be4a1734 Admin/Cygwin/README
--- a/Admin/Cygwin/README	Tue May 22 16:59:27 2012 +0200
+++ b/Admin/Cygwin/README	Wed May 23 12:02:27 2012 +0200
@@ -11,7 +11,7 @@
 http://cygwin.com/ml/cygwin/2012-04/msg00415.html
 http://cygwin.com/ml/cygwin/2012-04/msg00417.html
 
-* Mirror with many old versions (not setup.init!)
+* Mirror with many old versions (not setup.ini)
   http://ftp.eq.uc.pt/software/pc/prog/cygwin
 
 * Time machine for older versions:
diff -r d2bdd85ee23c -r c5f7be4a1734 Admin/Cygwin/init.bat
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Cygwin/init.bat	Wed May 23 12:02:27 2012 +0200
@@ -0,0 +1,8 @@
+@echo off
+
+cd "%~dp0"
+cd "..\.."
+
+echo Initializing ...
+"contrib\cygwin-1.7.9\bin\ash" /bin/rebaseall
+"contrib\cygwin-1.7.9\bin\bash" -c "PATH=/bin; chmod -wx $(find heaps -type f); mkpasswd -l >/etc/passwd; mkgroup -l >/etc/group"
diff -r d2bdd85ee23c -r c5f7be4a1734 Admin/Cygwin/sfx.txt
--- a/Admin/Cygwin/sfx.txt	Tue May 22 16:59:27 2012 +0200
+++ b/Admin/Cygwin/sfx.txt	Wed May 23 12:02:27 2012 +0200
@@ -5,4 +5,5 @@
 ExtractPathText="Target directory"
 ExtractTitle="Unpacking Isabelle2012 ..."
 Shortcut="Du,{%%T\Isabelle2012\Isabelle.exe},{},{},{},{},{%%T\Isabelle2012}"
+RunProgram="\"%%T\Isabelle2012\contrib\cygwin-1.7.9\init.bat\""
 ;!@InstallEnd@!
diff -r d2bdd85ee23c -r c5f7be4a1734 Admin/launch4j/Isabelle.exe
Binary file Admin/launch4j/Isabelle.exe has changed
diff -r d2bdd85ee23c -r c5f7be4a1734 Admin/launch4j/isabelle.xml
--- a/Admin/launch4j/isabelle.xml	Tue May 22 16:59:27 2012 +0200
+++ b/Admin/launch4j/isabelle.xml	Wed May 23 12:02:27 2012 +0200
@@ -15,12 +15,12 @@
   <icon>isabelle.ico</icon>
   <classPath>
     <mainClass>isabelle.Main</mainClass>
-    <cp>lib\classes\ext\Pure.jar</cp>
-    <cp>lib\classes\ext\scala-library.jar</cp>
-    <cp>lib\classes\ext\scala-swing.jar</cp>
+    <cp>%EXEDIR%\lib\classes\ext\Pure.jar</cp>
+    <cp>%EXEDIR%\lib\classes\ext\scala-library.jar</cp>
+    <cp>%EXEDIR%\lib\classes\ext\scala-swing.jar</cp>
   </classPath>
   <jre>
-    <path>contrib\jdk-6u31_x86-cygwin\jdk1.6.0_31</path>
+    <path>%EXEDIR%\contrib\jdk-6u31_x86-cygwin\jdk1.6.0_31</path>
     <minVersion></minVersion>
     <maxVersion></maxVersion>
     <jdkPreference>jdkOnly</jdkPreference>
diff -r d2bdd85ee23c -r c5f7be4a1734 NEWS
--- a/NEWS	Tue May 22 16:59:27 2012 +0200
+++ b/NEWS	Wed May 23 12:02:27 2012 +0200
@@ -758,6 +758,9 @@
 * New theory HOL/Library/DAList provides an abstract type for
 association lists with distinct keys.
 
+* Session HOL/IMP: Added new theory of abstract interpretation of
+annotated commands.
+
 * Session HOL-Import: Re-implementation from scratch is faster,
 simpler, and more scalable.  Requires a proof bundle, which is
 available as an external component.  Discontinued old (and mostly
diff -r d2bdd85ee23c -r c5f7be4a1734 doc-src/Main/Docs/Main_Doc.thy
--- a/doc-src/Main/Docs/Main_Doc.thy	Tue May 22 16:59:27 2012 +0200
+++ b/doc-src/Main/Docs/Main_Doc.thy	Wed May 23 12:02:27 2012 +0200
@@ -26,7 +26,7 @@
 text{*
 
 \begin{abstract}
-This document lists the main types, functions and syntax provided by theory @{theory Main}. It is meant as a quick overview of what is available. The sophisticated class structure is only hinted at. For details see \url{http://isabelle.in.tum.de/dist/library/HOL/}.
+This document lists the main types, functions and syntax provided by theory @{theory Main}. It is meant as a quick overview of what is available. The sophisticated class structure is only hinted at. For details see \url{http://isabelle.in.tum.de/library/HOL/}.
 \end{abstract}
 
 \section{HOL}
diff -r d2bdd85ee23c -r c5f7be4a1734 doc-src/Main/Docs/document/Main_Doc.tex
--- a/doc-src/Main/Docs/document/Main_Doc.tex	Tue May 22 16:59:27 2012 +0200
+++ b/doc-src/Main/Docs/document/Main_Doc.tex	Wed May 23 12:02:27 2012 +0200
@@ -30,7 +30,7 @@
 %
 \begin{isamarkuptext}%
 \begin{abstract}
-This document lists the main types, functions and syntax provided by theory \isa{Main}. It is meant as a quick overview of what is available. The sophisticated class structure is only hinted at. For details see \url{http://isabelle.in.tum.de/dist/library/HOL/}.
+This document lists the main types, functions and syntax provided by theory \isa{Main}. It is meant as a quick overview of what is available. The sophisticated class structure is only hinted at. For details see \url{http://isabelle.in.tum.de/library/HOL/}.
 \end{abstract}
 
 \section{HOL}
diff -r d2bdd85ee23c -r c5f7be4a1734 lib/Tools/display
--- a/lib/Tools/display	Tue May 22 16:59:27 2012 +0200
+++ b/lib/Tools/display	Wed May 23 12:02:27 2012 +0200
@@ -74,6 +74,7 @@
   PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$FILE")
   mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
   $VIEWER "$PRIVATE_FILE"
+  sleep 5   #try to avoid races
   rm -f "$PRIVATE_FILE"
 else
   exec $VIEWER "$FILE"
diff -r d2bdd85ee23c -r c5f7be4a1734 lib/scripts/feeder.pl
--- a/lib/scripts/feeder.pl	Tue May 22 16:59:27 2012 +0200
+++ b/lib/scripts/feeder.pl	Wed May 23 12:02:27 2012 +0200
@@ -11,8 +11,6 @@
 
 # setup signal handlers
 
-sub hangup { exit(0); }
-$SIG{'HUP'} = "hangup";
 $SIG{'INT'} = "IGNORE";
 
 
diff -r d2bdd85ee23c -r c5f7be4a1734 src/HOL/Isar_Examples/Group_Context.thy
--- a/src/HOL/Isar_Examples/Group_Context.thy	Tue May 22 16:59:27 2012 +0200
+++ b/src/HOL/Isar_Examples/Group_Context.thy	Wed May 23 12:02:27 2012 +0200
@@ -55,10 +55,10 @@
   finally show "x ** one = x" .
 qed
 
-lemma one_equality: "e ** x = x \<Longrightarrow> one = e"
+lemma one_equality:
+  assumes eq: "e ** x = x"
+  shows "one = e"
 proof -
-  fix e x
-  assume eq: "e ** x = x"
   have "one = x ** inverse x"
     by (simp only: right_inverse)
   also have "\<dots> = (e ** x) ** inverse x"
@@ -72,10 +72,10 @@
   finally show "one = e" .
 qed
 
-lemma inverse_equality: "x' ** x = one \<Longrightarrow> inverse x = x'"
+lemma inverse_equality:
+  assumes eq: "x' ** x = one"
+  shows "inverse x = x'"
 proof -
-  fix x x'
-  assume eq: "x' ** x = one"
   have "inverse x = one ** inverse x"
     by (simp only: left_one)
   also have "\<dots> = (x' ** x) ** inverse x"
diff -r d2bdd85ee23c -r c5f7be4a1734 src/HOL/Isar_Examples/ROOT.ML
--- a/src/HOL/Isar_Examples/ROOT.ML	Tue May 22 16:59:27 2012 +0200
+++ b/src/HOL/Isar_Examples/ROOT.ML	Wed May 23 12:02:27 2012 +0200
@@ -5,14 +5,17 @@
 use_thys [
   "Basic_Logic",
   "Cantor",
-  "Peirce",
   "Drinker",
   "Expr_Compiler",
+  "Fibonacci",
   "Group",
-  "Summation",
+  "Group_Context",
+  "Group_Notepad",
+  "Hoare_Ex",
   "Knaster_Tarski",
   "Mutilated_Checkerboard",
+  "Nested_Datatype",
+  "Peirce",
   "Puzzle",
-  "Nested_Datatype",
-  "Hoare_Ex"
+  "Summation"
 ];
diff -r d2bdd85ee23c -r c5f7be4a1734 src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Tue May 22 16:59:27 2012 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Wed May 23 12:02:27 2012 +0200
@@ -1066,7 +1066,7 @@
         Symtab.update ("true", (@{term True}, booleanN)),
         Name.context),
        thy |> Sign.add_path
-         (if prfx = "" then Long_Name.base_name ident else prfx)) |>
+         ((if prfx = "" then "" else prfx ^ "__") ^ Long_Name.base_name ident)) |>
       fold (add_type_def prfx) (items types) |>
       fold (snd oo add_const prfx) consts' |> (fn ids_thy as ((tab, _), _) =>
         ids_thy |>
diff -r d2bdd85ee23c -r c5f7be4a1734 src/HOL/Tools/ATP/atp_problem_generate.ML
diff -r d2bdd85ee23c -r c5f7be4a1734 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Tue May 22 16:59:27 2012 +0200
+++ b/src/HOL/Tools/inductive.ML	Wed May 23 12:02:27 2012 +0200
@@ -469,7 +469,7 @@
             fun list_ex ([], t) = t
               | list_ex ((a, T) :: vars, t) =
                   HOLogic.exists_const T $ Abs (a, T, list_ex (vars, t));
-            val conjs = map2 (curry HOLogic.mk_eq) frees us @ (map HOLogic.dest_Trueprop ts);
+            val conjs = map2 (curry HOLogic.mk_eq) frees us @ map HOLogic.dest_Trueprop ts;
           in
             list_ex (params', if null conjs then @{term True} else foldr1 HOLogic.mk_conj conjs)
           end;
@@ -479,26 +479,30 @@
           else foldr1 HOLogic.mk_disj (map mk_intr_conj c_intrs);
         val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
         fun prove_intr1 (i, _) = Subgoal.FOCUS_PREMS (fn {params, prems, ...} =>
-            let
-              val (prems', last_prem) = split_last prems;
-            in
-              EVERY1 (select_disj (length c_intrs) (i + 1)) THEN
-              EVERY (replicate (length params) (rtac @{thm exI} 1)) THEN
-              EVERY (map (fn prem => (rtac @{thm conjI} 1 THEN rtac prem 1)) prems') THEN
-              rtac last_prem 1
-            end) ctxt' 1;
+            EVERY1 (select_disj (length c_intrs) (i + 1)) THEN
+            EVERY (replicate (length params) (rtac @{thm exI} 1)) THEN
+            (if null prems then rtac @{thm TrueI} 1
+             else
+              let
+                val (prems', last_prem) = split_last prems;
+              in
+                EVERY (map (fn prem => (rtac @{thm conjI} 1 THEN rtac prem 1)) prems') THEN
+                rtac last_prem 1
+              end)) ctxt' 1;
         fun prove_intr2 (((_, _, us, _), ts, params'), intr) =
           EVERY (replicate (length params') (etac @{thm exE} 1)) THEN
-          EVERY (replicate (length ts + length us - 1) (etac @{thm conjE} 1)) THEN
-          Subgoal.FOCUS_PREMS (fn {params, prems, ...} =>
-            let
-              val (eqs, prems') = chop (length us) prems;
-              val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs;
-            in
-              rewrite_goal_tac rew_thms 1 THEN
-              rtac intr 1 THEN
-              EVERY (map (fn p => rtac p 1) prems')
-            end) ctxt' 1;
+          (if null ts andalso null us then rtac intr 1
+           else
+            EVERY (replicate (length ts + length us - 1) (etac @{thm conjE} 1)) THEN
+            Subgoal.FOCUS_PREMS (fn {params, prems, ...} =>
+              let
+                val (eqs, prems') = chop (length us) prems;
+                val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs;
+              in
+                rewrite_goal_tac rew_thms 1 THEN
+                rtac intr 1 THEN
+                EVERY (map (fn p => rtac p 1) prems')
+              end) ctxt' 1);
       in
         Skip_Proof.prove ctxt' [] [] eq (fn _ =>
           rtac @{thm iffI} 1 THEN etac (#1 elim) 1 THEN
diff -r d2bdd85ee23c -r c5f7be4a1734 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue May 22 16:59:27 2012 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed May 23 12:02:27 2012 +0200
@@ -188,7 +188,7 @@
   | _ => raise UNDEF);
 
 fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
-  | end_theory pos (State (NONE, _)) = error ("Missing theory" ^ Position.str_of pos)
+  | end_theory pos (State (NONE, _)) = error ("Bad theory" ^ Position.str_of pos)
   | end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.str_of pos);
 
 
diff -r d2bdd85ee23c -r c5f7be4a1734 src/Pure/System/main.scala
--- a/src/Pure/System/main.scala	Tue May 22 16:59:27 2012 +0200
+++ b/src/Pure/System/main.scala	Wed May 23 12:02:27 2012 +0200
@@ -21,11 +21,9 @@
       }
       catch { case exn: Throwable => (Exn.message(exn), 2) }
 
-    if (rc != 0) {
-      val text = new TextArea(out + "\nReturn code: " + rc)
-      text.editable = false
-      Library.dialog(null, "Isabelle", "Isabelle output", text)
-    }
+    if (rc != 0)
+      Library.dialog(null, "Isabelle", "Isabelle output",
+        Library.scrollable_text(out + "\nReturn code: " + rc))
 
     System.exit(rc)
   }
diff -r d2bdd85ee23c -r c5f7be4a1734 src/Pure/library.scala
--- a/src/Pure/library.scala	Tue May 22 16:59:27 2012 +0200
+++ b/src/Pure/library.scala	Wed May 23 12:02:27 2012 +0200
@@ -12,7 +12,7 @@
 import java.awt.Component
 import javax.swing.JOptionPane
 
-import scala.swing.ComboBox
+import scala.swing.{ComboBox, TextArea, ScrollPane}
 import scala.swing.event.SelectionChanged
 import scala.collection.mutable
 
@@ -130,6 +130,14 @@
 
   /* simple dialogs */
 
+  def scrollable_text(txt: String, width: Int = 76, editable: Boolean = false): ScrollPane =
+  {
+    val text = new TextArea(txt)
+    if (width > 0) text.columns = width
+    text.editable = editable
+    new ScrollPane(text)
+  }
+
   private def simple_dialog(kind: Int, default_title: String,
     parent: Component, title: String, message: Seq[Any])
   {
diff -r d2bdd85ee23c -r c5f7be4a1734 src/Tools/JVM/java_ext_dirs
--- a/src/Tools/JVM/java_ext_dirs	Tue May 22 16:59:27 2012 +0200
+++ b/src/Tools/JVM/java_ext_dirs	Wed May 23 12:02:27 2012 +0200
@@ -17,7 +17,7 @@
 
 ## main
 
-isabelle_jdk java \
+isabelle_jdk java -Dfile.encoding=UTF-8 \
   -classpath "$(jvmpath "$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs.jar")" \
   isabelle.Java_Ext_Dirs "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")" 2>/dev/null
 
diff -r d2bdd85ee23c -r c5f7be4a1734 src/Tools/jEdit/src/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Tue May 22 16:59:27 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Wed May 23 12:02:27 2012 +0200
@@ -40,7 +40,8 @@
   override def click(view: View) = {
     Isabelle_System.source_file(Path.explode(def_file)) match {
       case None =>
-        Library.error_dialog(view, "File not found", "Could not find source file " + def_file)
+        Library.error_dialog(view, "File not found",
+          Library.scrollable_text("Could not find source file " + def_file))
       case Some(file) =>
         jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + def_line))
     }
diff -r d2bdd85ee23c -r c5f7be4a1734 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue May 22 16:59:27 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Wed May 23 12:02:27 2012 +0200
@@ -388,9 +388,9 @@
           phase match {
             case Session.Failed =>
               Swing_Thread.later {
-                val text = new scala.swing.TextArea(Isabelle.session.current_syslog())
-                text.editable = false
-                Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
+                Library.error_dialog(jEdit.getActiveView,
+                  "Failed to start Isabelle process",
+                    Library.scrollable_text(Isabelle.session.current_syslog()))
               }
 
             case Session.Ready =>