src/HOL/Nitpick.thy
changeset 55415 05f5fdb8d093
parent 55414 eab03e9cee8a
child 55539 0819931d652d
     1.1 --- a/src/HOL/Nitpick.thy	Wed Feb 12 08:35:57 2014 +0100
     1.2 +++ b/src/HOL/Nitpick.thy	Wed Feb 12 08:35:57 2014 +0100
     1.3 @@ -104,8 +104,8 @@
     1.4  
     1.5  declare unit.cases [nitpick_simp del]
     1.6  
     1.7 -lemma nat_case_unfold [nitpick_unfold]:
     1.8 -"nat_case x f n \<equiv> if n = 0 then x else f (n - 1)"
     1.9 +lemma case_nat_unfold [nitpick_unfold]:
    1.10 +"case_nat x f n \<equiv> if n = 0 then x else f (n - 1)"
    1.11  apply (rule eq_reflection)
    1.12  by (cases n) auto
    1.13  
    1.14 @@ -241,7 +241,7 @@
    1.15  hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word
    1.16  hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold
    1.17      prod_def refl'_def wf'_def card'_def setsum'_def
    1.18 -    fold_graph'_def The_psimp Eps_psimp case_unit_unfold nat_case_unfold
    1.19 +    fold_graph'_def The_psimp Eps_psimp case_unit_unfold case_nat_unfold
    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