src/HOL/Nitpick.thy
changeset 47909 5f1afeebafbc
parent 46950 d0181abdbdac
child 47988 e4b69e10b990
     1.1 --- a/src/HOL/Nitpick.thy	Thu May 10 22:00:24 2012 +0200
     1.2 +++ b/src/HOL/Nitpick.thy	Fri May 11 00:45:24 2012 +0200
     1.3 @@ -72,6 +72,10 @@
     1.4  "tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}"
     1.5  by (simp add: trancl_def)
     1.6  
     1.7 +lemma [nitpick_simp, no_atp]:
     1.8 +"of_nat n = (if n = 0 then 0 else 1 + of_nat (n - 1))"
     1.9 +by (case_tac n) auto
    1.10 +
    1.11  definition prod :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
    1.12  "prod A B = {(a, b). a \<in> A \<and> b \<in> B}"
    1.13  
    1.14 @@ -93,7 +97,7 @@
    1.15  
    1.16  text {*
    1.17  The following lemmas are not strictly necessary but they help the
    1.18 -\textit{special\_level} optimization.
    1.19 +\textit{specialize} optimization.
    1.20  *}
    1.21  
    1.22  lemma The_psimp [nitpick_psimp, no_atp]: