--- a/src/HOL/Nitpick.thy Thu May 10 22:00:24 2012 +0200
+++ b/src/HOL/Nitpick.thy Fri May 11 00:45:24 2012 +0200
@@ -72,6 +72,10 @@
"tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}"
by (simp add: trancl_def)
+lemma [nitpick_simp, no_atp]:
+"of_nat n = (if n = 0 then 0 else 1 + of_nat (n - 1))"
+by (case_tac n) auto
+
definition prod :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
"prod A B = {(a, b). a \<in> A \<and> b \<in> B}"
@@ -93,7 +97,7 @@
text {*
The following lemmas are not strictly necessary but they help the
-\textit{special\_level} optimization.
+\textit{specialize} optimization.
*}
lemma The_psimp [nitpick_psimp, no_atp]: