src/HOL/Nitpick.thy
 changeset 61076 bdc1e2f0a86a parent 60758 d8d85a8172b5 child 61121 efe8b18306b7
```     1.1 --- a/src/HOL/Nitpick.thy	Tue Sep 01 17:25:36 2015 +0200
1.2 +++ b/src/HOL/Nitpick.thy	Tue Sep 01 22:32:58 2015 +0200
1.3 @@ -72,7 +72,7 @@
1.4  definition card' :: "'a set \<Rightarrow> nat" where
1.5    "card' A \<equiv> if finite A then length (SOME xs. set xs = A \<and> distinct xs) else 0"
1.6
1.7 -definition setsum' :: "('a \<Rightarrow> 'b\<Colon>comm_monoid_add) \<Rightarrow> 'a set \<Rightarrow> 'b" where
1.8 +definition setsum' :: "('a \<Rightarrow> 'b::comm_monoid_add) \<Rightarrow> 'a set \<Rightarrow> 'b" where
1.9    "setsum' f A \<equiv> if finite A then listsum (map f (SOME xs. set xs = A \<and> distinct xs)) else 0"
1.10
1.11  inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool" where
1.12 @@ -193,7 +193,7 @@
1.13  definition less_eq_frac :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
1.14    [nitpick_simp]: "less_eq_frac q r \<longleftrightarrow> num (plus_frac q (uminus_frac r)) \<le> 0"
1.15
1.16 -definition of_frac :: "'a \<Rightarrow> 'b\<Colon>{inverse,ring_1}" where
1.17 +definition of_frac :: "'a \<Rightarrow> 'b::{inverse,ring_1}" where
1.18    "of_frac q \<equiv> of_int (num q) / of_int (denom q)"
1.19
1.20  axiomatization wf_wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
```