1.1 --- a/Admin/isatest/isatest-makedist	Wed Mar 27 20:57:05 2013 +0100
     1.2 +++ b/Admin/isatest/isatest-makedist	Wed Mar 27 21:07:10 2013 +0100
     1.3 @@ -112,7 +112,8 @@
     1.4    $MAKEALL $HOME/settings/mac-poly64-M4;
     1.5    $MAKEALL $HOME/settings/mac-poly64-M8;
     1.6    $MAKEALL $HOME/settings/mac-poly-M4;
     1.7 -  $MAKEALL $HOME/settings/mac-poly-M8"
     1.8 +  $MAKEALL $HOME/settings/mac-poly-M8;
     1.9 +  $MAKEALL $HOME/settings/mac-poly-M8-skip_proofs"
    1.10  sleep 15
    1.11  $SSH macbroy6 "$MAKEALL $HOME/settings/mac-poly64-M2"
    1.12  sleep 15

     2.1 --- a/Admin/isatest/isatest-stats	Wed Mar 27 20:57:05 2013 +0100
     2.2 +++ b/Admin/isatest/isatest-stats	Wed Mar 27 21:07:10 2013 +0100
     2.3 @@ -6,7 +6,7 @@
     2.4  
     2.5  THIS="$(cd "$(dirname "$0")"; pwd)"
     2.6  
     2.7 -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"
     2.8 +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"
     2.9  
    2.10  ISABELLE_SESSIONS="
    2.11    HOL

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/Admin/isatest/settings/mac-poly-M8-skip_proofs	Wed Mar 27 21:07:10 2013 +0100
     3.3 @@ -0,0 +1,31 @@
     3.4 +# -*- shell-script -*- :mode=shellscript:
     3.5 +
     3.6 +init_components /home/isabelle/contrib "$HOME/admin/components/main"
     3.7 +
     3.8 +  POLYML_HOME="/home/polyml/polyml-5.5.0"
     3.9 +  ML_SYSTEM="polyml-5.5.0"
    3.10 +  ML_PLATFORM="x86-darwin"
    3.11 +  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
    3.12 +  ML_OPTIONS="-H 1000 --gcthreads 8"
    3.13 +
    3.14 +
    3.15 +ISABELLE_HOME_USER=~/isabelle-mac-poly-M8-skip_proofs
    3.16 +
    3.17 +# Where to look for isabelle tools (multiple dirs separated by ':').
    3.18 +ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
    3.19 +
    3.20 +# Location for temporary files (should be on a local file system).
    3.21 +ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
    3.22 +
    3.23 +
    3.24 +# Heap input locations. ML system identifier is included in lookup.
    3.25 +ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
    3.26 +
    3.27 +# Heap output location. ML system identifier is appended automatically later on.
    3.28 +ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
    3.29 +ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
    3.30 +
    3.31 +ISABELLE_BUILD_OPTIONS="threads=8 skip_proofs"
    3.32 +
    3.33 +Z3_NON_COMMERCIAL="yes"
    3.34 +

     4.1 --- a/src/HOL/ROOT	Wed Mar 27 20:57:05 2013 +0100
     4.2 +++ b/src/HOL/ROOT	Wed Mar 27 21:07:10 2013 +0100
     4.3 @@ -424,10 +424,6 @@
     4.4      "document/root.bib"
     4.5      "document/root.tex"
     4.6  
     4.7 -session "HOL-MicroJava-skip_proofs" in MicroJava = HOL +
     4.8 -  options [condition = ISABELLE_FULL_TEST, document = false, skip_proofs]
     4.9 -  theories MicroJava
    4.10 -
    4.11  session "HOL-NanoJava" in NanoJava = HOL +
    4.12    description {*
    4.13      Hoare Logic for a tiny fragment of Java.