src/HOL/Nitpick.thy
 changeset 35699 9ed327529a44 parent 35671 ed2c3830d881 child 35807 e4d1b5cbd429
```     1.1 --- a/src/HOL/Nitpick.thy	Wed Mar 10 17:46:28 2010 +0100
1.2 +++ b/src/HOL/Nitpick.thy	Wed Mar 10 19:21:59 2010 +0100
1.3 @@ -96,10 +96,10 @@
1.4                  else THE y. wfrec_rel R (%f x. F (Recdef.cut f R x) x) x y"
1.5
1.6  definition card' :: "('a \<Rightarrow> bool) \<Rightarrow> nat" where
1.7 -"card' X \<equiv> length (SOME xs. set xs = X \<and> distinct xs)"
1.8 +"card' A \<equiv> if finite A then length (safe_Eps (\<lambda>xs. set xs = A \<and> distinct xs)) else 0"
1.9
1.10  definition setsum' :: "('a \<Rightarrow> 'b\<Colon>comm_monoid_add) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b" where
1.11 -"setsum' f A \<equiv> if finite A then listsum (map f (SOME xs. set xs = A \<and> distinct xs)) else 0"
1.12 +"setsum' f A \<equiv> if finite A then listsum (map f (safe_Eps (\<lambda>xs. set xs = A \<and> distinct xs))) else 0"
1.13
1.14  inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool" where
1.15  "fold_graph' f z {} z" |
```