--- a/Admin/PLATFORMS Wed Sep 05 11:37:22 2012 +0200
+++ b/Admin/PLATFORMS Wed Sep 05 13:44:03 2012 +0200
@@ -68,9 +68,9 @@
x86-darwin personality usually works seamlessly for C/C++ programs,
but the Java 7 platform is only available for x86_64-darwin.
-Add-on executables are expected to without manual user configuration,
-Each component settings script needs to work out the platform details
-appropriately.
+Add-on executables are expected to work without manual user
+configuration. Each component settings script needs to determine the
+platform details appropriately.
The Isabelle settings environment provides the following variables to
help configuring platform-dependent tools:
@@ -88,8 +88,10 @@
Moreover note that ML and JVM usually have a different idea of the
platform, depending on the respective binaries that are actually run.
-Poly/ML 5.5.x runs most efficiently on 32 bit, even for large
-applications. The JVM usually performs better in 64 bit mode.
+Poly/ML 5.5.x performs best in 32 bit mode, even for large
+applications, thanks to its sophisticated heap management. The JVM
+usually works better in 64 bit mode, which allows its heap to grow
+beyond 2 GB.
The traditional "uname" Unix tool usually only tells about its own
executable format, not the underlying platform!
@@ -109,8 +111,8 @@
performs not as well in addressing various delicate details of
operating system concepts (processes, signals, sockets etc.).
-* Scala with Java 1.7. The Isabelle/Scala layer irons out many
- oddities and portability issues of the Java platform.
+* Scala with Java 1.7. Isabelle/Scala irons out many oddities and
+ portability issues of the Java platform.
Known problems
@@ -129,8 +131,7 @@
* The Java runtime has its own idea about the underlying platform,
which affects Java native libraries in particular. In
- Isabelle/Scala isabelle.Platform.jvm_platform identifies the JVM
- platform. Since there can be many different Java installations on
- the same machine, which can also be run with different options,
- reliable JVM platform identification works from inside the running
- JVM only.
+ Isabelle/Scala the function isabelle.Platform.jvm_platform
+ identifies the JVM platform. Since a particular Java version is
+ always bundled with Isabelle, the resulting settings also provide
+ some clues about its platform, without running it.
--- a/Admin/isatest/isatest-makedist Wed Sep 05 11:37:22 2012 +0200
+++ b/Admin/isatest/isatest-makedist Wed Sep 05 13:44:03 2012 +0200
@@ -116,7 +116,7 @@
sleep 15
$SSH macbroy6 "$MAKEALL $HOME/settings/mac-poly64-M2"
sleep 15
-$SSH macbroy30 "sleep 10800; $MAKEALL $HOME/settings/mac-poly-M2"
+$SSH macbroy30 "$MAKEALL $HOME/settings/mac-poly-M2"
echo ------------------- spawned tests successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
--- a/CONTRIBUTORS Wed Sep 05 11:37:22 2012 +0200
+++ b/CONTRIBUTORS Wed Sep 05 13:44:03 2012 +0200
@@ -6,6 +6,10 @@
Contributions to this Isabelle version
--------------------------------------
+* September 2012: Christian Sternagel, JAIST
+ Consolidated HOL/Library (theories: Prefix_Order, Sublist, and
+ Sublist_Order) w.r.t. prefixes, suffixes, and embedding on lists.
+
* August 2012: Dmitriy Traytel, Andrei Popescu, Jasmin Blanchette, TUM
New (co)datatype package.
--- a/NEWS Wed Sep 05 11:37:22 2012 +0200
+++ b/NEWS Wed Sep 05 13:44:03 2012 +0200
@@ -41,6 +41,51 @@
*** HOL ***
+* Renamed theory Library/List_Prefix to Library/Sublist.
+INCOMPATIBILITY. Related changes are:
+
+ - Renamed constants:
+
+ prefix ~> prefixeq
+ strict_prefix ~> prefix
+
+ Renamed lemmas accordingly, INCOMPATIBILITY.
+
+ - Replaced constant "postfix" by "suffixeq" with swapped argument order
+ (i.e., "postfix xs ys" is now "suffixeq ys xs") and dropped old infix
+ syntax "xs >>= ys"; use "suffixeq ys xs" instead. Renamed lemmas
+ accordingly. INCOMPATIBILITY.
+
+ - New constant "emb" for homeomorphic embedding on lists. New
+ abbreviation "sub" for special case "emb (op =)".
+
+ - Library/Sublist does no longer provide "order" and "bot" type class
+ instances for the prefix order (merely corresponding locale
+ interpretations). The type class instances are to be found in
+ Library/Prefix_Order. INCOMPATIBILITY.
+
+ - The sublist relation from Library/Sublist_Order is now based on
+ "Sublist.sub". Replaced lemmas:
+
+ le_list_append_le_same_iff ~> Sublist.sub_append_le_same_iff
+ le_list_append_mono ~> Sublist.emb_append_mono
+ le_list_below_empty ~> Sublist.emb_Nil, Sublist.emb_Nil2
+ le_list_Cons_EX ~> Sublist.emb_ConsD
+ le_list_drop_Cons2 ~> Sublist.sub_Cons2'
+ le_list_drop_Cons_neq ~> Sublist.sub_Cons2_neq
+ le_list_drop_Cons ~> Sublist.sub_Cons'
+ le_list_drop_many ~> Sublist.sub_drop_many
+ le_list_filter_left ~> Sublist.sub_filter_left
+ le_list_rev_drop_many ~> Sublist.sub_rev_drop_many
+ le_list_rev_take_iff ~> Sublist.sub_append
+ le_list_same_length ~> Sublist.sub_same_length
+ le_list_take_many_iff ~> Sublist.sub_append'
+ less_eq_list.drop ~> less_eq_list_drop
+ less_eq_list.induct ~> less_eq_list_induct
+ not_le_list_length ~> Sublist.not_sub_length
+
+ INCOMPATIBILITY.
+
* HOL/Codatatype: New (co)datatype package with support for mixed,
nested recursion and interesting non-free datatypes.