# HG changeset patch
# User nipkow
# Date 1373008623 -7200
# Node ID 1e09c034d6c39a8514c2c6f69ce4e7b13d79dd2f
# Parent  bc6e0144726a17372bd995fb55d1f85e2b362da7
tund proofs

diff -r bc6e0144726a -r 1e09c034d6c3 src/HOL/IMP/Abs_Int1_parity.thy
--- a/src/HOL/IMP/Abs_Int1_parity.thy	Thu Jul 04 12:02:11 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1_parity.thy	Fri Jul 05 09:17:03 2013 +0200
@@ -116,8 +116,7 @@
   txt{* Warning: this subproof refers to the names @{text a1} and @{text a2}
   from the statement of the axiom. *}
   case goal4 thus ?case
-  proof(cases a1 a2 rule: parity.exhaust[case_product parity.exhaust])
-  qed (auto simp add:mod_add_eq)
+    by (induction a1 a2 rule: plus_parity.induct) (auto simp add:mod_add_eq)
 qed
 
 text{* Instantiating the abstract interpretation locale requires no more
@@ -159,9 +158,8 @@
 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
 proof
   case goal1 thus ?case
-  proof(cases a1 a2 b1 b2
-   rule: parity.exhaust[case_product parity.exhaust[case_product parity.exhaust[case_product parity.exhaust]]]) (* FIXME - UGLY! *)
-  qed (auto simp add:less_eq_parity_def)
+    by(induction a1 a2 rule: plus_parity.induct)
+      (auto simp add:less_eq_parity_def)
 qed
 
 definition m_parity :: "parity \<Rightarrow> nat" where