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"