--- a/src/HOL/Nitpick.thy Wed Mar 10 17:46:28 2010 +0100
+++ b/src/HOL/Nitpick.thy Wed Mar 10 19:21:59 2010 +0100
@@ -96,10 +96,10 @@
else THE y. wfrec_rel R (%f x. F (Recdef.cut f R x) x) x y"
definition card' :: "('a \<Rightarrow> bool) \<Rightarrow> nat" where
-"card' X \<equiv> length (SOME xs. set xs = X \<and> distinct xs)"
+"card' A \<equiv> if finite A then length (safe_Eps (\<lambda>xs. set xs = A \<and> distinct xs)) else 0"
definition setsum' :: "('a \<Rightarrow> 'b\<Colon>comm_monoid_add) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b" where
-"setsum' f A \<equiv> if finite A then listsum (map f (SOME xs. set xs = A \<and> distinct xs)) else 0"
+"setsum' f A \<equiv> if finite A then listsum (map f (safe_Eps (\<lambda>xs. set xs = A \<and> distinct xs))) else 0"
inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool" where
"fold_graph' f z {} z" |
--- a/src/HOL/Nitpick_Examples/Mini_Nits.thy Wed Mar 10 17:46:28 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy Wed Mar 10 19:21:59 2010 +0100
@@ -24,8 +24,6 @@
fun unknown n t = (minipick n t = "unknown" orelse raise FAIL)
*}
-ML {* minipick 1 @{prop "\<forall>x\<Colon>'a. \<exists>y\<Colon>'b. f x = y"} *}
-
ML {* genuine 1 @{prop "x = Not"} *}
ML {* none 1 @{prop "\<exists>x. x = Not"} *}
ML {* none 1 @{prop "\<not> False"} *}
--- a/src/HOL/Tools/Nitpick/minipick.ML Wed Mar 10 17:46:28 2010 +0100
+++ b/src/HOL/Tools/Nitpick/minipick.ML Wed Mar 10 19:21:59 2010 +0100
@@ -336,7 +336,8 @@
val max_solutions = 1
in
case solve_any_problem overlord NONE max_threads max_solutions problems of
- NotInstalled => "unknown"
+ JavaNotInstalled => "unknown"
+ | KodkodiNotInstalled => "unknown"
| Normal ([], _, _) => "none"
| Normal _ => "genuine"
| TimedOut _ => "unknown"