--- a/Admin/isatest/isatest-makedist Wed Mar 27 21:12:49 2013 +0100
+++ b/Admin/isatest/isatest-makedist Wed Mar 27 21:13:02 2013 +0100
@@ -112,7 +112,8 @@
$MAKEALL $HOME/settings/mac-poly64-M4;
$MAKEALL $HOME/settings/mac-poly64-M8;
$MAKEALL $HOME/settings/mac-poly-M4;
- $MAKEALL $HOME/settings/mac-poly-M8"
+ $MAKEALL $HOME/settings/mac-poly-M8;
+ $MAKEALL $HOME/settings/mac-poly-M8-skip_proofs"
sleep 15
$SSH macbroy6 "$MAKEALL $HOME/settings/mac-poly64-M2"
sleep 15
--- a/Admin/isatest/isatest-stats Wed Mar 27 21:12:49 2013 +0100
+++ b/Admin/isatest/isatest-stats Wed Mar 27 21:13:02 2013 +0100
@@ -6,7 +6,7 @@
THIS="$(cd "$(dirname "$0")"; pwd)"
-PLATFORMS="at-poly at-poly-test afp at64-poly mac-poly-M2 mac-poly-M4 mac-poly64-M2 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at-sml-dev"
+PLATFORMS="at-poly at-poly-test afp at64-poly mac-poly-M2 mac-poly-M4 mac-poly64-M2 mac-poly64-M4 mac-poly-M8 mac-poly-M8-skip_proofs mac-poly64-M8 at-sml-dev"
ISABELLE_SESSIONS="
HOL
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest/settings/mac-poly-M8-skip_proofs Wed Mar 27 21:13:02 2013 +0100
@@ -0,0 +1,31 @@
+# -*- shell-script -*- :mode=shellscript:
+
+init_components /home/isabelle/contrib "$HOME/admin/components/main"
+
+ POLYML_HOME="/home/polyml/polyml-5.5.0"
+ ML_SYSTEM="polyml-5.5.0"
+ ML_PLATFORM="x86-darwin"
+ ML_HOME="$POLYML_HOME/$ML_PLATFORM"
+ ML_OPTIONS="-H 1000 --gcthreads 8"
+
+
+ISABELLE_HOME_USER=~/isabelle-mac-poly-M8-skip_proofs
+
+# Where to look for isabelle tools (multiple dirs separated by ':').
+ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
+
+# Location for temporary files (should be on a local file system).
+ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
+
+
+# Heap input locations. ML system identifier is included in lookup.
+ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
+
+# Heap output location. ML system identifier is appended automatically later on.
+ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
+ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
+
+ISABELLE_BUILD_OPTIONS="threads=8 skip_proofs"
+
+Z3_NON_COMMERCIAL="yes"
+
--- a/src/HOL/ROOT Wed Mar 27 21:12:49 2013 +0100
+++ b/src/HOL/ROOT Wed Mar 27 21:13:02 2013 +0100
@@ -424,10 +424,6 @@
"document/root.bib"
"document/root.tex"
-session "HOL-MicroJava-skip_proofs" in MicroJava = HOL +
- options [condition = ISABELLE_FULL_TEST, document = false, skip_proofs]
- theories MicroJava
-
session "HOL-NanoJava" in NanoJava = HOL +
description {*
Hoare Logic for a tiny fragment of Java.