1.1 --- a/src/HOL/Nitpick.thy	Tue Mar 09 09:25:23 2010 +0100
     1.2 +++ b/src/HOL/Nitpick.thy	Tue Mar 09 14:18:21 2010 +0100
     1.3 @@ -36,7 +36,8 @@
     1.4             and bisim :: "bisim_iterator \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
     1.5             and bisim_iterator_max :: bisim_iterator
     1.6             and Quot :: "'a \<Rightarrow> 'b"
     1.7 -           and Tha :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
     1.8 +           and safe_The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
     1.9 +           and safe_Eps :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
    1.10  
    1.11  datatype ('a, 'b) fin_fun = FinFun "('a \<Rightarrow> 'b)"
    1.12  datatype ('a, 'b) fun_box = FunBox "('a \<Rightarrow> 'b)"
    1.13 @@ -237,10 +238,11 @@
    1.14  setup {* Nitpick_Isar.setup *}
    1.15  
    1.16  hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim 
    1.17 -    bisim_iterator_max Quot Tha FinFun FunBox PairBox Word refl' wf' wf_wfrec
    1.18 -    wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm
    1.19 -    Frac Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac plus_frac
    1.20 -    times_frac uminus_frac number_of_frac inverse_frac less_eq_frac of_frac
    1.21 +    bisim_iterator_max Quot safe_The safe_Eps FinFun FunBox PairBox Word refl'
    1.22 +    wf' wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm
    1.23 +    int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom
    1.24 +    norm_frac frac plus_frac times_frac uminus_frac number_of_frac inverse_frac
    1.25 +    less_eq_frac of_frac
    1.26  hide (open) type bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
    1.27      word
    1.28  hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def