--- a/src/HOL/Nitpick.thy Wed Jan 20 10:38:19 2010 +0100
+++ b/src/HOL/Nitpick.thy Wed Jan 20 11:54:19 2010 +0100
@@ -29,10 +29,13 @@
typedecl bisim_iterator
axiomatization unknown :: 'a
+ and is_unknown :: "'a \<Rightarrow> bool"
and undefined_fast_The :: 'a
and undefined_fast_Eps :: 'a
and bisim :: "bisim_iterator \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
and bisim_iterator_max :: bisim_iterator
+ and Quot :: "'a \<Rightarrow> 'b"
+ and quot_normal :: "'a \<Rightarrow> 'a"
and Tha :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
datatype ('a, 'b) pair_box = PairBox 'a 'b
@@ -246,11 +249,12 @@
setup {* Nitpick_Isar.setup *}
-hide (open) const unknown undefined_fast_The undefined_fast_Eps bisim
- bisim_iterator_max Tha PairBox FunBox Word refl' wf' wf_wfrec wf_wfrec'
- wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac
- Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac plus_frac
- times_frac uminus_frac number_of_frac inverse_frac less_eq_frac of_frac
+hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim
+ bisim_iterator_max Quot quot_normal Tha PairBox FunBox Word refl' wf'
+ wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd
+ int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac
+ plus_frac times_frac uminus_frac number_of_frac inverse_frac less_eq_frac
+ of_frac
hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit word
hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
--- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Jan 20 10:38:19 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Jan 20 11:54:19 2010 +0100
@@ -320,8 +320,8 @@
val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
(* typ -> bool *)
fun is_type_always_monotonic T =
- ((not (is_pure_typedef thy T) orelse is_univ_typedef thy T) andalso
- not (is_quot_type thy T)) orelse
+ (is_datatype thy T andalso not (is_quot_type thy T) andalso
+ (not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
is_number_type thy T orelse is_bit_type T
fun is_type_monotonic T =
unique_scope orelse