# 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