1.1 --- a/src/HOL/Nitpick.thy	Mon Dec 14 16:48:49 2009 +0100
     1.2 +++ b/src/HOL/Nitpick.thy	Thu Dec 17 15:22:11 2009 +0100
     1.3 @@ -36,7 +36,12 @@
     1.4             and Tha :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
     1.5  
     1.6  datatype ('a, 'b) pair_box = PairBox 'a 'b
     1.7 -datatype ('a, 'b) fun_box = FunBox "'a \<Rightarrow> 'b"
     1.8 +datatype ('a, 'b) fun_box = FunBox "('a \<Rightarrow> 'b)"
     1.9 +
    1.10 +typedecl unsigned_bit
    1.11 +typedecl signed_bit
    1.12 +
    1.13 +datatype 'a word = Word "('a set)"
    1.14  
    1.15  text {*
    1.16  Alternative definitions.
    1.17 @@ -126,8 +131,6 @@
    1.18  
    1.19  declare nat.cases [nitpick_simp del]
    1.20  
    1.21 -lemmas [nitpick_def] = dvd_eq_mod_eq_0 [THEN eq_reflection]
    1.22 -
    1.23  lemma list_size_simp [nitpick_simp]:
    1.24  "list_size f xs = (if xs = [] then 0
    1.25                     else Suc (f (hd xs) + list_size f (tl xs)))"
    1.26 @@ -244,11 +247,11 @@
    1.27  setup {* Nitpick_Isar.setup *}
    1.28  
    1.29  hide (open) const unknown undefined_fast_The undefined_fast_Eps bisim 
    1.30 -    bisim_iterator_max Tha refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum'
    1.31 -    fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac
    1.32 -    one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
    1.33 -    number_of_frac inverse_frac less_eq_frac of_frac
    1.34 -hide (open) type bisim_iterator pair_box fun_box
    1.35 +    bisim_iterator_max Tha PairBox FunBox Word refl' wf' wf_wfrec wf_wfrec'
    1.36 +    wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac
    1.37 +    Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac plus_frac
    1.38 +    times_frac uminus_frac number_of_frac inverse_frac less_eq_frac of_frac
    1.39 +hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit word
    1.40  hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
    1.41      wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
    1.42      The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def