# HG changeset patch
# User haftmann
# Date 1413124303 -7200
# Node ID 3ccafeb9a1d167a55138d91dcf0aa2b3df860aec
# Parent  fce800afeec7e394c30bb082092ab5c20756c820
eliminiated clone

diff -r fce800afeec7 -r 3ccafeb9a1d1 src/HOL/IMPP/EvenOdd.thy
--- 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