1.1 --- a/.hgtags	Tue May 22 16:59:27 2012 +0200
     1.2 +++ b/.hgtags	Wed May 23 12:02:27 2012 +0200
     1.3 @@ -28,4 +28,4 @@
     1.4  35815ce9218a8822a50f5d80b96aa8d1970ec35d Isabelle2009-2
     1.5  6d736d983d5cfec4a6c6fba174db2cd93493a96b Isabelle2011
     1.6  76fef3e570043b84a32716b5633085d2fb215525 Isabelle2011-1
     1.7 -
     1.8 +21c42b095c841d1a7508c143d6b6e98d95dbfa69 Isabelle2012

     2.1 --- a/ANNOUNCE	Tue May 22 16:59:27 2012 +0200
     2.2 +++ b/ANNOUNCE	Wed May 23 12:02:27 2012 +0200
     2.3 @@ -3,10 +3,35 @@
     2.4  
     2.5  Isabelle2012 is now available.
     2.6  
     2.7 -This version significantly improves upon Isabelle2011-1, see the NEWS
     2.8 -file in the distribution for more details.  Some notable changes are:
     2.9 +This version introduces many changes and improvements over
    2.10 +Isabelle2011-1, see the NEWS file in the distribution for more
    2.11 +details.  Some highlights are:
    2.12  
    2.13 -* FIXME
    2.14 +* Improved Isabelle/jEdit Prover IDE (PIDE).
    2.15 +
    2.16 +* Support for block-structured specification contexts.
    2.17 +
    2.18 +* Discontinued old code generator.
    2.19 +
    2.20 +* Updated manuals: prog-prove, isar-ref, implementation, system.
    2.21 +
    2.22 +* HOL: type 'a set is proper type constructor again.
    2.23 +
    2.24 +* HOL: improved representation of numerals.
    2.25 +
    2.26 +* HOL: new transfer and lifting packages, improved quotient package.
    2.27 +
    2.28 +* HOL tool enhancements: Quickcheck, Nitpick, Sledgehammer.
    2.29 +
    2.30 +* HOL library enhancements, including HOL-Library and HOL-Probability.
    2.31 +
    2.32 +* HOL: more TPTP support.
    2.33 +
    2.34 +* Re-implementation of HOL-Import for HOL-Light.
    2.35 +
    2.36 +* ZF: some modernization of notation and proofs.
    2.37 +
    2.38 +* System integration: improved support of Windows platform.
    2.39  
    2.40  
    2.41  You may get Isabelle2012 from the following mirror sites:

     3.1 --- a/Admin/CHECKLIST	Tue May 22 16:59:27 2012 +0200
     3.2 +++ b/Admin/CHECKLIST	Wed May 23 12:02:27 2012 +0200
     3.3 @@ -67,10 +67,9 @@
     3.4  
     3.5  - makedist: REPOS_NAME="isabelle-release"
     3.6  
     3.7 -- hgrc: default = /home/isabelle-repository/repos/isabelle-release
     3.8 +- various .hg/hgrc files:
     3.9 +  default = /home/isabelle-repository/repos/isabelle-release
    3.10  
    3.11 -  isatest@macbroy28:hg-isabelle/.hg/hgrc
    3.12 -  isatest@atbroy102:hg-isabelle/.hg/hgrc
    3.13 -
    3.14 +- isatest@macbroy28:hg-isabelle/.hg/hgrc
    3.15  - isatest@macbroy28:devel-page/content/index.content
    3.16  

     4.1 --- a/Admin/Cygwin/README	Tue May 22 16:59:27 2012 +0200
     4.2 +++ b/Admin/Cygwin/README	Wed May 23 12:02:27 2012 +0200
     4.3 @@ -11,7 +11,7 @@
     4.4  http://cygwin.com/ml/cygwin/2012-04/msg00415.html
     4.5  http://cygwin.com/ml/cygwin/2012-04/msg00417.html
     4.6  
     4.7 -* Mirror with many old versions (not setup.init!)
     4.8 +* Mirror with many old versions (not setup.ini)
     4.9    http://ftp.eq.uc.pt/software/pc/prog/cygwin
    4.10  
    4.11  * Time machine for older versions:

     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/Admin/Cygwin/init.bat	Wed May 23 12:02:27 2012 +0200
     5.3 @@ -0,0 +1,8 @@
     5.4 +@echo off
     5.5 +
     5.6 +cd "%~dp0"
     5.7 +cd "..\.."
     5.8 +
     5.9 +echo Initializing ...
    5.10 +"contrib\cygwin-1.7.9\bin\ash" /bin/rebaseall
    5.11 +"contrib\cygwin-1.7.9\bin\bash" -c "PATH=/bin; chmod -wx $(find heaps -type f); mkpasswd -l >/etc/passwd; mkgroup -l >/etc/group"

     6.1 --- a/Admin/Cygwin/sfx.txt	Tue May 22 16:59:27 2012 +0200
     6.2 +++ b/Admin/Cygwin/sfx.txt	Wed May 23 12:02:27 2012 +0200
     6.3 @@ -5,4 +5,5 @@
     6.4  ExtractPathText="Target directory"
     6.5  ExtractTitle="Unpacking Isabelle2012 ..."
     6.6  Shortcut="Du,{%%T\Isabelle2012\Isabelle.exe},{},{},{},{},{%%T\Isabelle2012}"
     6.7 +RunProgram="\"%%T\Isabelle2012\contrib\cygwin-1.7.9\init.bat\""
     6.8  ;!@InstallEnd@!

     7.1 Binary file Admin/launch4j/Isabelle.exe has changed

     8.1 --- a/Admin/launch4j/isabelle.xml	Tue May 22 16:59:27 2012 +0200
     8.2 +++ b/Admin/launch4j/isabelle.xml	Wed May 23 12:02:27 2012 +0200
     8.3 @@ -15,12 +15,12 @@
     8.4    <icon>isabelle.ico</icon>
     8.5    <classPath>
     8.6      <mainClass>isabelle.Main</mainClass>
     8.7 -    <cp>lib\classes\ext\Pure.jar</cp>
     8.8 -    <cp>lib\classes\ext\scala-library.jar</cp>
     8.9 -    <cp>lib\classes\ext\scala-swing.jar</cp>
    8.10 +    <cp>%EXEDIR%\lib\classes\ext\Pure.jar</cp>
    8.11 +    <cp>%EXEDIR%\lib\classes\ext\scala-library.jar</cp>
    8.12 +    <cp>%EXEDIR%\lib\classes\ext\scala-swing.jar</cp>
    8.13    </classPath>
    8.14    <jre>
    8.15 -    <path>contrib\jdk-6u31_x86-cygwin\jdk1.6.0_31</path>
    8.16 +    <path>%EXEDIR%\contrib\jdk-6u31_x86-cygwin\jdk1.6.0_31</path>
    8.17      <minVersion></minVersion>
    8.18      <maxVersion></maxVersion>
    8.19      <jdkPreference>jdkOnly</jdkPreference>

     9.1 --- a/NEWS	Tue May 22 16:59:27 2012 +0200
     9.2 +++ b/NEWS	Wed May 23 12:02:27 2012 +0200
     9.3 @@ -758,6 +758,9 @@
     9.4  * New theory HOL/Library/DAList provides an abstract type for
     9.5  association lists with distinct keys.
     9.6  
     9.7 +* Session HOL/IMP: Added new theory of abstract interpretation of
     9.8 +annotated commands.
     9.9 +
    9.10  * Session HOL-Import: Re-implementation from scratch is faster,
    9.11  simpler, and more scalable.  Requires a proof bundle, which is
    9.12  available as an external component.  Discontinued old (and mostly

    10.1 --- a/doc-src/Main/Docs/Main_Doc.thy	Tue May 22 16:59:27 2012 +0200
    10.2 +++ b/doc-src/Main/Docs/Main_Doc.thy	Wed May 23 12:02:27 2012 +0200
    10.3 @@ -26,7 +26,7 @@
    10.4  text{*
    10.5  
    10.6  \begin{abstract}
    10.7 -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/}.
    10.8 +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/}.
    10.9  \end{abstract}
   10.10  
   10.11  \section{HOL}

    11.1 --- a/doc-src/Main/Docs/document/Main_Doc.tex	Tue May 22 16:59:27 2012 +0200
    11.2 +++ b/doc-src/Main/Docs/document/Main_Doc.tex	Wed May 23 12:02:27 2012 +0200
    11.3 @@ -30,7 +30,7 @@
    11.4  %
    11.5  \begin{isamarkuptext}%
    11.6  \begin{abstract}
    11.7 -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/}.
    11.8 +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/}.
    11.9  \end{abstract}
   11.10  
   11.11  \section{HOL}

    12.1 --- a/lib/Tools/display	Tue May 22 16:59:27 2012 +0200
    12.2 +++ b/lib/Tools/display	Wed May 23 12:02:27 2012 +0200
    12.3 @@ -74,6 +74,7 @@
    12.4    PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$FILE")
    12.5    mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
    12.6    $VIEWER "$PRIVATE_FILE"
    12.7 +  sleep 5   #try to avoid races
    12.8    rm -f "$PRIVATE_FILE"
    12.9  else
   12.10    exec $VIEWER "$FILE"

    13.1 --- a/lib/scripts/feeder.pl	Tue May 22 16:59:27 2012 +0200
    13.2 +++ b/lib/scripts/feeder.pl	Wed May 23 12:02:27 2012 +0200
    13.3 @@ -11,8 +11,6 @@
    13.4  
    13.5  # setup signal handlers
    13.6  
    13.7 -sub hangup { exit(0); }
    13.8 -$SIG{'HUP'} = "hangup";
    13.9  $SIG{'INT'} = "IGNORE";
   13.10  
   13.11  

    14.1 --- a/src/HOL/Isar_Examples/Group_Context.thy	Tue May 22 16:59:27 2012 +0200
    14.2 +++ b/src/HOL/Isar_Examples/Group_Context.thy	Wed May 23 12:02:27 2012 +0200
    14.3 @@ -55,10 +55,10 @@
    14.4    finally show "x ** one = x" .
    14.5  qed
    14.6  
    14.7 -lemma one_equality: "e ** x = x \<Longrightarrow> one = e"
    14.8 +lemma one_equality:
    14.9 +  assumes eq: "e ** x = x"
   14.10 +  shows "one = e"
   14.11  proof -
   14.12 -  fix e x
   14.13 -  assume eq: "e ** x = x"
   14.14    have "one = x ** inverse x"
   14.15      by (simp only: right_inverse)
   14.16    also have "\<dots> = (e ** x) ** inverse x"
   14.17 @@ -72,10 +72,10 @@
   14.18    finally show "one = e" .
   14.19  qed
   14.20  
   14.21 -lemma inverse_equality: "x' ** x = one \<Longrightarrow> inverse x = x'"
   14.22 +lemma inverse_equality:
   14.23 +  assumes eq: "x' ** x = one"
   14.24 +  shows "inverse x = x'"
   14.25  proof -
   14.26 -  fix x x'
   14.27 -  assume eq: "x' ** x = one"
   14.28    have "inverse x = one ** inverse x"
   14.29      by (simp only: left_one)
   14.30    also have "\<dots> = (x' ** x) ** inverse x"

    15.1 --- a/src/HOL/Isar_Examples/ROOT.ML	Tue May 22 16:59:27 2012 +0200
    15.2 +++ b/src/HOL/Isar_Examples/ROOT.ML	Wed May 23 12:02:27 2012 +0200
    15.3 @@ -5,14 +5,17 @@
    15.4  use_thys [
    15.5    "Basic_Logic",
    15.6    "Cantor",
    15.7 -  "Peirce",
    15.8    "Drinker",
    15.9    "Expr_Compiler",
   15.10 +  "Fibonacci",
   15.11    "Group",
   15.12 -  "Summation",
   15.13 +  "Group_Context",
   15.14 +  "Group_Notepad",
   15.15 +  "Hoare_Ex",
   15.16    "Knaster_Tarski",
   15.17    "Mutilated_Checkerboard",
   15.18 +  "Nested_Datatype",
   15.19 +  "Peirce",
   15.20    "Puzzle",
   15.21 -  "Nested_Datatype",
   15.22 -  "Hoare_Ex"
   15.23 +  "Summation"
   15.24  ];

    16.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Tue May 22 16:59:27 2012 +0200
    16.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Wed May 23 12:02:27 2012 +0200
    16.3 @@ -1066,7 +1066,7 @@
    16.4          Symtab.update ("true", (@{term True}, booleanN)),
    16.5          Name.context),
    16.6         thy |> Sign.add_path
    16.7 -         (if prfx = "" then Long_Name.base_name ident else prfx)) |>
    16.8 +         ((if prfx = "" then "" else prfx ^ "__") ^ Long_Name.base_name ident)) |>
    16.9        fold (add_type_def prfx) (items types) |>
   16.10        fold (snd oo add_const prfx) consts' |> (fn ids_thy as ((tab, _), _) =>
   16.11          ids_thy |>

    17.1 --- a/src/HOL/Tools/inductive.ML	Tue May 22 16:59:27 2012 +0200
    17.2 +++ b/src/HOL/Tools/inductive.ML	Wed May 23 12:02:27 2012 +0200
    17.3 @@ -469,7 +469,7 @@
    17.4              fun list_ex ([], t) = t
    17.5                | list_ex ((a, T) :: vars, t) =
    17.6                    HOLogic.exists_const T $ Abs (a, T, list_ex (vars, t));
    17.7 -            val conjs = map2 (curry HOLogic.mk_eq) frees us @ (map HOLogic.dest_Trueprop ts);
    17.8 +            val conjs = map2 (curry HOLogic.mk_eq) frees us @ map HOLogic.dest_Trueprop ts;
    17.9            in
   17.10              list_ex (params', if null conjs then @{term True} else foldr1 HOLogic.mk_conj conjs)
   17.11            end;
   17.12 @@ -479,26 +479,30 @@
   17.13            else foldr1 HOLogic.mk_disj (map mk_intr_conj c_intrs);
   17.14          val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   17.15          fun prove_intr1 (i, _) = Subgoal.FOCUS_PREMS (fn {params, prems, ...} =>
   17.16 -            let
   17.17 -              val (prems', last_prem) = split_last prems;
   17.18 -            in
   17.19 -              EVERY1 (select_disj (length c_intrs) (i + 1)) THEN
   17.20 -              EVERY (replicate (length params) (rtac @{thm exI} 1)) THEN
   17.21 -              EVERY (map (fn prem => (rtac @{thm conjI} 1 THEN rtac prem 1)) prems') THEN
   17.22 -              rtac last_prem 1
   17.23 -            end) ctxt' 1;
   17.24 +            EVERY1 (select_disj (length c_intrs) (i + 1)) THEN
   17.25 +            EVERY (replicate (length params) (rtac @{thm exI} 1)) THEN
   17.26 +            (if null prems then rtac @{thm TrueI} 1
   17.27 +             else
   17.28 +              let
   17.29 +                val (prems', last_prem) = split_last prems;
   17.30 +              in
   17.31 +                EVERY (map (fn prem => (rtac @{thm conjI} 1 THEN rtac prem 1)) prems') THEN
   17.32 +                rtac last_prem 1
   17.33 +              end)) ctxt' 1;
   17.34          fun prove_intr2 (((_, _, us, _), ts, params'), intr) =
   17.35            EVERY (replicate (length params') (etac @{thm exE} 1)) THEN
   17.36 -          EVERY (replicate (length ts + length us - 1) (etac @{thm conjE} 1)) THEN
   17.37 -          Subgoal.FOCUS_PREMS (fn {params, prems, ...} =>
   17.38 -            let
   17.39 -              val (eqs, prems') = chop (length us) prems;
   17.40 -              val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs;
   17.41 -            in
   17.42 -              rewrite_goal_tac rew_thms 1 THEN
   17.43 -              rtac intr 1 THEN
   17.44 -              EVERY (map (fn p => rtac p 1) prems')
   17.45 -            end) ctxt' 1;
   17.46 +          (if null ts andalso null us then rtac intr 1
   17.47 +           else
   17.48 +            EVERY (replicate (length ts + length us - 1) (etac @{thm conjE} 1)) THEN
   17.49 +            Subgoal.FOCUS_PREMS (fn {params, prems, ...} =>
   17.50 +              let
   17.51 +                val (eqs, prems') = chop (length us) prems;
   17.52 +                val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs;
   17.53 +              in
   17.54 +                rewrite_goal_tac rew_thms 1 THEN
   17.55 +                rtac intr 1 THEN
   17.56 +                EVERY (map (fn p => rtac p 1) prems')
   17.57 +              end) ctxt' 1);
   17.58        in
   17.59          Skip_Proof.prove ctxt' [] [] eq (fn _ =>
   17.60            rtac @{thm iffI} 1 THEN etac (#1 elim) 1 THEN

    18.1 --- a/src/Pure/Isar/toplevel.ML	Tue May 22 16:59:27 2012 +0200
    18.2 +++ b/src/Pure/Isar/toplevel.ML	Wed May 23 12:02:27 2012 +0200
    18.3 @@ -188,7 +188,7 @@
    18.4    | _ => raise UNDEF);
    18.5  
    18.6  fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
    18.7 -  | end_theory pos (State (NONE, _)) = error ("Missing theory" ^ Position.str_of pos)
    18.8 +  | end_theory pos (State (NONE, _)) = error ("Bad theory" ^ Position.str_of pos)
    18.9    | end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.str_of pos);
   18.10  
   18.11  

    19.1 --- a/src/Pure/System/main.scala	Tue May 22 16:59:27 2012 +0200
    19.2 +++ b/src/Pure/System/main.scala	Wed May 23 12:02:27 2012 +0200
    19.3 @@ -21,11 +21,9 @@
    19.4        }
    19.5        catch { case exn: Throwable => (Exn.message(exn), 2) }
    19.6  
    19.7 -    if (rc != 0) {
    19.8 -      val text = new TextArea(out + "\nReturn code: " + rc)
    19.9 -      text.editable = false
   19.10 -      Library.dialog(null, "Isabelle", "Isabelle output", text)
   19.11 -    }
   19.12 +    if (rc != 0)
   19.13 +      Library.dialog(null, "Isabelle", "Isabelle output",
   19.14 +        Library.scrollable_text(out + "\nReturn code: " + rc))
   19.15  
   19.16      System.exit(rc)
   19.17    }

    20.1 --- a/src/Pure/library.scala	Tue May 22 16:59:27 2012 +0200
    20.2 +++ b/src/Pure/library.scala	Wed May 23 12:02:27 2012 +0200
    20.3 @@ -12,7 +12,7 @@
    20.4  import java.awt.Component
    20.5  import javax.swing.JOptionPane
    20.6  
    20.7 -import scala.swing.ComboBox
    20.8 +import scala.swing.{ComboBox, TextArea, ScrollPane}
    20.9  import scala.swing.event.SelectionChanged
   20.10  import scala.collection.mutable
   20.11  
   20.12 @@ -130,6 +130,14 @@
   20.13  
   20.14    /* simple dialogs */
   20.15  
   20.16 +  def scrollable_text(txt: String, width: Int = 76, editable: Boolean = false): ScrollPane =
   20.17 +  {
   20.18 +    val text = new TextArea(txt)
   20.19 +    if (width > 0) text.columns = width
   20.20 +    text.editable = editable
   20.21 +    new ScrollPane(text)
   20.22 +  }
   20.23 +
   20.24    private def simple_dialog(kind: Int, default_title: String,
   20.25      parent: Component, title: String, message: Seq[Any])
   20.26    {

    21.1 --- a/src/Tools/JVM/java_ext_dirs	Tue May 22 16:59:27 2012 +0200
    21.2 +++ b/src/Tools/JVM/java_ext_dirs	Wed May 23 12:02:27 2012 +0200
    21.3 @@ -17,7 +17,7 @@
    21.4  
    21.5  ## main
    21.6  
    21.7 -isabelle_jdk java \
    21.8 +isabelle_jdk java -Dfile.encoding=UTF-8 \
    21.9    -classpath "$(jvmpath "$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs.jar")" \
   21.10    isabelle.Java_Ext_Dirs "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")" 2>/dev/null
   21.11  

    22.1 --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Tue May 22 16:59:27 2012 +0200
    22.2 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Wed May 23 12:02:27 2012 +0200
    22.3 @@ -40,7 +40,8 @@
    22.4    override def click(view: View) = {
    22.5      Isabelle_System.source_file(Path.explode(def_file)) match {
    22.6        case None =>
    22.7 -        Library.error_dialog(view, "File not found", "Could not find source file " + def_file)
    22.8 +        Library.error_dialog(view, "File not found",
    22.9 +          Library.scrollable_text("Could not find source file " + def_file))
   22.10        case Some(file) =>
   22.11          jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + def_line))
   22.12      }

    23.1 --- a/src/Tools/jEdit/src/plugin.scala	Tue May 22 16:59:27 2012 +0200
    23.2 +++ b/src/Tools/jEdit/src/plugin.scala	Wed May 23 12:02:27 2012 +0200
    23.3 @@ -388,9 +388,9 @@
    23.4            phase match {
    23.5              case Session.Failed =>
    23.6                Swing_Thread.later {
    23.7 -                val text = new scala.swing.TextArea(Isabelle.session.current_syslog())
    23.8 -                text.editable = false
    23.9 -                Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
   23.10 +                Library.error_dialog(jEdit.getActiveView,
   23.11 +                  "Failed to start Isabelle process",
   23.12 +                    Library.scrollable_text(Isabelle.session.current_syslog()))
   23.13                }
   23.14  
   23.15              case Session.Ready =>