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
```