1.1 --- a/src/HOL/Nitpick.thy	Mon Mar 08 15:20:40 2010 -0800
     1.2 +++ b/src/HOL/Nitpick.thy	Tue Mar 09 09:25:23 2010 +0100
     1.3 @@ -38,8 +38,9 @@
     1.4             and Quot :: "'a \<Rightarrow> 'b"
     1.5             and Tha :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
     1.6  
     1.7 +datatype ('a, 'b) fin_fun = FinFun "('a \<Rightarrow> 'b)"
     1.8 +datatype ('a, 'b) fun_box = FunBox "('a \<Rightarrow> 'b)"
     1.9  datatype ('a, 'b) pair_box = PairBox 'a 'b
    1.10 -datatype ('a, 'b) fun_box = FunBox "('a \<Rightarrow> 'b)"
    1.11  
    1.12  typedecl unsigned_bit
    1.13  typedecl signed_bit
    1.14 @@ -220,8 +221,8 @@
    1.15  use "Tools/Nitpick/kodkod_sat.ML"
    1.16  use "Tools/Nitpick/nitpick_util.ML"
    1.17  use "Tools/Nitpick/nitpick_hol.ML"
    1.18 +use "Tools/Nitpick/nitpick_mono.ML"
    1.19  use "Tools/Nitpick/nitpick_preproc.ML"
    1.20 -use "Tools/Nitpick/nitpick_mono.ML"
    1.21  use "Tools/Nitpick/nitpick_scope.ML"
    1.22  use "Tools/Nitpick/nitpick_peephole.ML"
    1.23  use "Tools/Nitpick/nitpick_rep.ML"
    1.24 @@ -236,11 +237,12 @@
    1.25  setup {* Nitpick_Isar.setup *}
    1.26  
    1.27  hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim 
    1.28 -    bisim_iterator_max Quot Tha PairBox FunBox Word refl' wf' wf_wfrec wf_wfrec'
    1.29 -    wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac
    1.30 -    Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac plus_frac
    1.31 +    bisim_iterator_max Quot Tha FinFun FunBox PairBox Word refl' wf' wf_wfrec
    1.32 +    wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm
    1.33 +    Frac Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac plus_frac
    1.34      times_frac uminus_frac number_of_frac inverse_frac less_eq_frac of_frac
    1.35 -hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit word
    1.36 +hide (open) type bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
    1.37 +    word
    1.38  hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
    1.39      wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
    1.40      The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def