--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Mon Feb 22 14:36:10 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Mon Feb 22 19:31:00 2010 +0100
@@ -11,8 +11,8 @@
imports Main Rational
begin
-nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s,
- card = 1\<midarrow>4]
+nitpick_params [card = 1\<midarrow>4, sat_solver = MiniSat_JNI, max_threads = 1,
+ timeout = 60 s]
typedef three = "{0\<Colon>nat, 1, 2}"
by blast
@@ -138,7 +138,8 @@
by (rule Inl_Rep_not_Inr_Rep)
lemma "Abs_Sum (Rep_Sum a) = a"
-nitpick [card = 1\<midarrow>2, timeout = 60 s, expect = none]
+nitpick [card = 1, expect = none]
+nitpick [card = 2, expect = none]
by (rule Rep_Sum_inverse)
lemma "0::nat \<equiv> Abs_Nat Zero_Rep"