merged, abandoning change of src/HOL/Tools/ATP/atp_problem_generate.ML from 6ea205a4d7fd;
--- 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
--- 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:
--- 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
--- 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:
--- /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"
--- 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@!
Binary file Admin/launch4j/Isabelle.exe has changed
--- 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>
--- 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
--- 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}
--- 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}
--- 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"
--- 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";
--- 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"
--- 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"
];
--- 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 |>
--- 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
--- 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);
--- 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)
}
--- 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])
{
--- 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
--- 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))
}
--- 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 =>