src/HOL/Nitpick.thy
changeset 41052 3db267a01c1d
parent 41046 f2e94005d283
child 41792 ff3cb0c418b7
     1.1 --- a/src/HOL/Nitpick.thy	Tue Dec 07 11:56:01 2010 +0100
     1.2 +++ b/src/HOL/Nitpick.thy	Tue Dec 07 11:56:53 2010 +0100
     1.3 @@ -35,7 +35,6 @@
     1.4             and Quot :: "'a \<Rightarrow> 'b"
     1.5             and safe_The :: "('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  
    1.11 @@ -240,12 +239,11 @@
    1.12  setup {* Nitpick_Isar.setup *}
    1.13  
    1.14  hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The
    1.15 -    FinFun FunBox PairBox Word prod refl' wf' wf_wfrec wf_wfrec' wfrec' card'
    1.16 -    setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac
    1.17 -    zero_frac one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
    1.18 +    FunBox PairBox Word prod refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum'
    1.19 +    fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac
    1.20 +    one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
    1.21      number_of_frac inverse_frac less_frac less_eq_frac of_frac
    1.22 -hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
    1.23 -    word
    1.24 +hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word
    1.25  hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def prod_def
    1.26      refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def
    1.27      fold_graph'_def The_psimp Eps_psimp unit_case_def nat_case_def