# HG changeset patch
# User haftmann
# Date 1413136393 -7200
# Node ID cfdd09041638d28d932376f5f1be729bf24a67e5
# Parent  1ddba8bcbb58dc3c6a72870140f3fb9e70537b15
leftover from 3ccafeb9a1d1

diff -r 1ddba8bcbb58 -r cfdd09041638 src/HOL/IMPP/EvenOdd.thy
--- a/src/HOL/IMPP/EvenOdd.thy	Sun Oct 12 17:05:35 2014 +0200
+++ b/src/HOL/IMPP/EvenOdd.thy	Sun Oct 12 19:53:13 2014 +0200
@@ -41,23 +41,6 @@
   "Res_ok = (%Z s. even Z = (s<Res> = 0))"
 
 
-subsection "even"
-
-lemma not_even_1 [simp]: "even (Suc 0) = False"
-apply (unfold even_def)
-apply simp
-done
-
-lemma even_step [simp]: "even (Suc (Suc n)) = even n"
-apply (unfold even_def)
-apply (subgoal_tac "Suc (Suc n) = n+2")
-prefer 2
-apply  simp
-apply (erule ssubst)
-apply (rule dvd_reduce)
-done
-
-
 subsection "Arg, Res"
 
 declare Arg_neq_Res [simp] Arg_neq_Res [THEN not_sym, simp]