src/HOL/Nitpick.thy
changeset 47988 e4b69e10b990
parent 47909 5f1afeebafbc
child 48891 c0eafbd55de3
     1.1 --- a/src/HOL/Nitpick.thy	Thu May 24 17:05:30 2012 +0200
     1.2 +++ b/src/HOL/Nitpick.thy	Thu May 24 17:25:53 2012 +0200
     1.3 @@ -74,7 +74,7 @@
     1.4  
     1.5  lemma [nitpick_simp, no_atp]:
     1.6  "of_nat n = (if n = 0 then 0 else 1 + of_nat (n - 1))"
     1.7 -by (case_tac n) auto
     1.8 +by (cases n) auto
     1.9  
    1.10  definition prod :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
    1.11  "prod A B = {(a, b). a \<in> A \<and> b \<in> B}"
    1.12 @@ -106,7 +106,7 @@
    1.13  
    1.14  lemma Eps_psimp [nitpick_psimp, no_atp]:
    1.15  "\<lbrakk>P x; \<not> P y; Eps P = y\<rbrakk> \<Longrightarrow> Eps P = x"
    1.16 -apply (case_tac "P (Eps P)")
    1.17 +apply (cases "P (Eps P)")
    1.18   apply auto
    1.19  apply (erule contrapos_np)
    1.20  by (rule someI)
    1.21 @@ -122,7 +122,7 @@
    1.22  lemma nat_case_unfold [nitpick_unfold, no_atp]:
    1.23  "nat_case x f n \<equiv> if n = 0 then x else f (n - 1)"
    1.24  apply (rule eq_reflection)
    1.25 -by (case_tac n) auto
    1.26 +by (cases n) auto
    1.27  
    1.28  declare nat.cases [nitpick_simp del]
    1.29  
    1.30 @@ -130,7 +130,7 @@
    1.31  "list_size f xs = (if xs = [] then 0
    1.32                     else Suc (f (hd xs) + list_size f (tl xs)))"
    1.33  "size xs = (if xs = [] then 0 else Suc (size (tl xs)))"
    1.34 -by (case_tac xs) auto
    1.35 +by (cases xs) auto
    1.36  
    1.37  text {*
    1.38  Auxiliary definitions used to provide an alternative representation for