# HG changeset patch
# User wenzelm
# Date 1343829050 -7200
# Node ID bfce940c6f388e9bc57b856e148704a61453e244
# Parent  30a6e841390ad342f5001d9efd3927bb01df7c9d
clarified ISABELLE_FULL_TEST;

diff -r 30a6e841390a -r bfce940c6f38 Admin/isatest/isatest-makedist
--- a/Admin/isatest/isatest-makedist	Wed Aug 01 15:46:45 2012 +0200
+++ b/Admin/isatest/isatest-makedist	Wed Aug 01 15:50:50 2012 +0200
@@ -110,8 +110,8 @@
 $SSH macbroy23 "$MAKEALL $HOME/settings/at-poly-e"
 sleep 15
 $SSH macbroy2 "
-  env ISABELLE_BENCHMARK=true $MAKEALL $HOME/settings/mac-poly64-M4;
-  env ISABELLE_BENCHMARK=true $MAKEALL $HOME/settings/mac-poly64-M8;
+  $MAKEALL $HOME/settings/mac-poly64-M4;
+  $MAKEALL $HOME/settings/mac-poly64-M8;
   $MAKEALL $HOME/settings/mac-poly-M4;
   $MAKEALL $HOME/settings/mac-poly-M8"
 sleep 15
diff -r 30a6e841390a -r bfce940c6f38 Admin/isatest/settings/mac-poly64-M4
--- a/Admin/isatest/settings/mac-poly64-M4	Wed Aug 01 15:46:45 2012 +0200
+++ b/Admin/isatest/settings/mac-poly64-M4	Wed Aug 01 15:50:50 2012 +0200
@@ -26,4 +26,6 @@
 ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 4 -q 2"
 ISABELLE_BUILD_OPTIONS="browser_info=false document=false threads=4 parallel_proofs=2"
 
+ISABELLE_FULL_TEST=true
+
 init_component "$HOME/contrib_devel/kodkodi-1.2.16"
diff -r 30a6e841390a -r bfce940c6f38 Admin/isatest/settings/mac-poly64-M8
--- a/Admin/isatest/settings/mac-poly64-M8	Wed Aug 01 15:46:45 2012 +0200
+++ b/Admin/isatest/settings/mac-poly64-M8	Wed Aug 01 15:50:50 2012 +0200
@@ -26,5 +26,7 @@
 ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 8 -q 2"
 ISABELLE_BUILD_OPTIONS="browser_info=false document=false threads=8 parallel_proofs=2"
 
+ISABELLE_FULL_TEST=true
+
 init_component "$HOME/contrib_devel/kodkodi-1.2.16"
 
diff -r 30a6e841390a -r bfce940c6f38 src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Aug 01 15:46:45 2012 +0200
+++ b/src/HOL/ROOT	Wed Aug 01 15:50:50 2012 +0200
@@ -740,7 +740,7 @@
     Quickcheck_Narrowing_Examples
 
 session Quickcheck_Benchmark = HOL +
-  theories [condition = ISABELLE_BENCHMARK, quick_and_dirty]
+  theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]
     Find_Unused_Assms_Examples
     Needham_Schroeder_No_Attacker_Example
     Needham_Schroeder_Guided_Attacker_Example
@@ -874,7 +874,7 @@
 session Datatype_Benchmark = HOL +
   description {* Some rather large datatype examples (from John Harrison). *}
   options [document = false]
-  theories [condition = ISABELLE_BENCHMARK, timing]
+  theories [condition = ISABELLE_FULL_TEST, timing]
     Brackin
     Instructions
     SML
@@ -883,6 +883,6 @@
 session Record_Benchmark = HOL +
   description {* Some benchmark on large record. *}
   options [document = false]
-  theories [condition = ISABELLE_BENCHMARK, timing]
+  theories [condition = ISABELLE_FULL_TEST, timing]
     Record_Benchmark