src/HOL/Nitpick.thy
changeset 55642 63beb38e9258
parent 55539 0819931d652d
child 56643 41d3596d8a64
     1.1 --- a/src/HOL/Nitpick.thy	Fri Feb 21 00:09:55 2014 +0100
     1.2 +++ b/src/HOL/Nitpick.thy	Fri Feb 21 00:09:56 2014 +0100
     1.3 @@ -101,17 +101,17 @@
     1.4  lemma case_unit_unfold [nitpick_unfold]:
     1.5  "case_unit x u \<equiv> x"
     1.6  apply (subgoal_tac "u = ()")
     1.7 - apply (simp only: unit.cases)
     1.8 + apply (simp only: unit.case)
     1.9  by simp
    1.10  
    1.11 -declare unit.cases [nitpick_simp del]
    1.12 +declare unit.case [nitpick_simp del]
    1.13  
    1.14  lemma case_nat_unfold [nitpick_unfold]:
    1.15  "case_nat x f n \<equiv> if n = 0 then x else f (n - 1)"
    1.16  apply (rule eq_reflection)
    1.17  by (cases n) auto
    1.18  
    1.19 -declare nat.cases [nitpick_simp del]
    1.20 +declare nat.case [nitpick_simp del]
    1.21  
    1.22  lemma list_size_simp [nitpick_simp]:
    1.23  "list_size f xs = (if xs = [] then 0