--- a/src/HOL/IMP/Abs_Int1_parity.thy Thu Mar 07 18:14:30 2013 +0100
+++ b/src/HOL/IMP/Abs_Int1_parity.thy Fri Mar 08 11:28:04 2013 +0100
@@ -173,9 +173,7 @@
proof
case goal1 thus ?case by(auto simp add: m_parity_def less_eq_parity_def)
next
- case goal2 thus ?case by(auto simp add: m_parity_def less_eq_parity_def)
-next
- case goal3 thus ?case by(auto simp add: m_parity_def less_eq_parity_def less_parity_def)
+ case goal2 thus ?case by(auto simp add: m_parity_def less_eq_parity_def less_parity_def)
qed
thm AI_Some_measure