# HG changeset patch
# User wenzelm
# Date 1373026146 -7200
# Node ID b6a224676c04e957d112d53305824b92248cdf57
# Parent  1e09c034d6c39a8514c2c6f69ce4e7b13d79dd2f# Parent  dbac84eab3bc53eb496e78f7ef74cbb18644a387
merged

diff -r dbac84eab3bc -r b6a224676c04 src/HOL/IMP/Abs_Int1_parity.thy
--- a/src/HOL/IMP/Abs_Int1_parity.thy	Thu Jul 04 23:51:47 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1_parity.thy	Fri Jul 05 14:09:06 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