--- a/Admin/isatest/settings/at-mac-poly-5.1-para Wed Feb 10 14:12:30 2010 +0100
+++ b/Admin/isatest/settings/at-mac-poly-5.1-para Wed Feb 10 14:12:40 2010 +0100
@@ -25,3 +25,4 @@
ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 4 -q 2"
+unset KODKODI
--- a/Admin/isatest/settings/at-poly-5.1-para-e Wed Feb 10 14:12:30 2010 +0100
+++ b/Admin/isatest/settings/at-poly-5.1-para-e Wed Feb 10 14:12:40 2010 +0100
@@ -24,3 +24,5 @@
ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -M 10"
+unset KODKODI
+
--- a/Admin/isatest/settings/at-poly-dev-e Wed Feb 10 14:12:30 2010 +0100
+++ b/Admin/isatest/settings/at-poly-dev-e Wed Feb 10 14:12:40 2010 +0100
@@ -24,3 +24,5 @@
ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
+unset KODKODI
+
--- a/Admin/isatest/settings/at-sml Wed Feb 10 14:12:30 2010 +0100
+++ b/Admin/isatest/settings/at-sml Wed Feb 10 14:12:40 2010 +0100
@@ -24,3 +24,5 @@
ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
+unset KODKODI
+
--- a/Admin/isatest/settings/at-sml-dev-e Wed Feb 10 14:12:30 2010 +0100
+++ b/Admin/isatest/settings/at-sml-dev-e Wed Feb 10 14:12:40 2010 +0100
@@ -24,3 +24,5 @@
ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
+unset KODKODI
+
--- a/Admin/isatest/settings/at-sml-dev-p Wed Feb 10 14:12:30 2010 +0100
+++ b/Admin/isatest/settings/at-sml-dev-p Wed Feb 10 14:12:40 2010 +0100
@@ -24,3 +24,5 @@
ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
+unset KODKODI
+
--- a/Admin/isatest/settings/at64-poly Wed Feb 10 14:12:30 2010 +0100
+++ b/Admin/isatest/settings/at64-poly Wed Feb 10 14:12:40 2010 +0100
@@ -24,3 +24,5 @@
ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
+unset KODKODI
+
--- a/Admin/isatest/settings/at64-poly-5.1-para Wed Feb 10 14:12:30 2010 +0100
+++ b/Admin/isatest/settings/at64-poly-5.1-para Wed Feb 10 14:12:40 2010 +0100
@@ -24,3 +24,5 @@
ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -M 2"
+unset KODKODI
+
--- a/Admin/isatest/settings/at64-sml-dev Wed Feb 10 14:12:30 2010 +0100
+++ b/Admin/isatest/settings/at64-sml-dev Wed Feb 10 14:12:40 2010 +0100
@@ -24,3 +24,5 @@
ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
+unset KODKODI
+
--- a/Admin/isatest/settings/mac-poly64-M8 Wed Feb 10 14:12:30 2010 +0100
+++ b/Admin/isatest/settings/mac-poly64-M8 Wed Feb 10 14:12:40 2010 +0100
@@ -25,3 +25,5 @@
ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 8 -q 2"
+unset KODKODI
+
--- a/Admin/isatest/settings/mac-sml-dev Wed Feb 10 14:12:30 2010 +0100
+++ b/Admin/isatest/settings/mac-sml-dev Wed Feb 10 14:12:40 2010 +0100
@@ -24,3 +24,5 @@
ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
+unset KODKODI
+
--- a/Admin/isatest/settings/sun-poly Wed Feb 10 14:12:30 2010 +0100
+++ b/Admin/isatest/settings/sun-poly Wed Feb 10 14:12:40 2010 +0100
@@ -25,3 +25,5 @@
#ISABELLE_USEDIR_OPTIONS="-i true -d dvi -g true -v true"
ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -t true -M 6 -q 2"
+unset KODKODI
+
--- a/Admin/isatest/settings/sun-sml Wed Feb 10 14:12:30 2010 +0100
+++ b/Admin/isatest/settings/sun-sml Wed Feb 10 14:12:40 2010 +0100
@@ -25,3 +25,5 @@
# ISABELLE_USEDIR_OPTIONS="-i true -d dvi -g true -v true"
ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
+unset KODKODI
+
--- a/Admin/isatest/settings/sun-sml-dev Wed Feb 10 14:12:30 2010 +0100
+++ b/Admin/isatest/settings/sun-sml-dev Wed Feb 10 14:12:40 2010 +0100
@@ -25,3 +25,5 @@
# ISABELLE_USEDIR_OPTIONS="-i true -d dvi -g true -v true"
ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
+unset KODKODI
+
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Feb 10 14:12:30 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Feb 10 14:12:40 2010 +0100
@@ -885,7 +885,7 @@
done
lemma "BinTree_rec l n (Node x y) = n x y (BinTree_rec l n x) (BinTree_rec l n y)"
-nitpick [card = 1\<midarrow>6, expect = none]
+nitpick [card = 1\<midarrow>5, expect = none]
apply simp
done