--- a/src/HOL/IMPP/EvenOdd.thy Sun Oct 12 16:31:28 2014 +0200
+++ b/src/HOL/IMPP/EvenOdd.thy Sun Oct 12 16:31:43 2014 +0200
@@ -5,13 +5,9 @@
header {* Example of mutually recursive procedures verified with Hoare logic *}
theory EvenOdd
-imports Misc
+imports Misc "~~/src/HOL/Parity"
begin
-definition
- even :: "nat => bool" where
- "even n = (2 dvd n)"
-
axiomatization
Even :: pname and
Odd :: pname
@@ -47,11 +43,6 @@
subsection "even"
-lemma even_0 [simp]: "even 0"
-apply (unfold even_def)
-apply simp
-done
-
lemma not_even_1 [simp]: "even (Suc 0) = False"
apply (unfold even_def)
apply simp