src/HOL/Nitpick.thy
changeset 37704 c6161bee8486
parent 37397 18000f9d783e
child 38393 7c045c03598f
     1.1 --- a/src/HOL/Nitpick.thy	Sat Jul 03 00:49:12 2010 +0200
     1.2 +++ b/src/HOL/Nitpick.thy	Sat Jul 03 00:50:35 2010 +0200
     1.3 @@ -69,9 +69,6 @@
     1.4   apply (erule_tac x = y in allE)
     1.5  by (auto simp: mem_def)
     1.6  
     1.7 -lemma split_def [nitpick_def]: "split f = (\<lambda>p. f (fst p) (snd p))"
     1.8 -by (simp add: prod_case_unfold split_def)
     1.9 -
    1.10  lemma rtrancl_def [nitpick_def, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
    1.11  by simp
    1.12  
    1.13 @@ -252,12 +249,12 @@
    1.14      less_frac less_eq_frac of_frac
    1.15  hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
    1.16      word
    1.17 -hide_fact (open) If_def Ex1_def split_def rtrancl_def rtranclp_def tranclp_def
    1.18 -    refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def
    1.19 -    fold_graph'_def The_psimp Eps_psimp unit_case_def nat_case_def
    1.20 -    list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
    1.21 -    zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
    1.22 -    plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
    1.23 -    inverse_frac_def less_frac_def less_eq_frac_def of_frac_def
    1.24 +hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
    1.25 +    wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
    1.26 +    The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
    1.27 +    nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
    1.28 +    num_def denom_def norm_frac_def frac_def plus_frac_def times_frac_def
    1.29 +    uminus_frac_def number_of_frac_def inverse_frac_def less_frac_def
    1.30 +    less_eq_frac_def of_frac_def
    1.31  
    1.32  end