# HG changeset patch
# User huffman
# Date 1187707967 -7200
# Node ID 54da7d61372d73e0e04ed8b3e72cef32ce68f439
# Parent  560e8ecdf633c63e3561e2e99321fb582f64731a
simplify proof of word_of_int

diff -r 560e8ecdf633 -r 54da7d61372d src/HOL/Word/WordArith.thy
--- a/src/HOL/Word/WordArith.thy	Tue Aug 21 13:30:38 2007 +0200
+++ b/src/HOL/Word/WordArith.thy	Tue Aug 21 16:52:47 2007 +0200
@@ -836,16 +836,8 @@
 
 lemma word_of_int: "of_int = word_of_int"
   apply (rule ext)
-  apply (unfold of_int_def)
-  apply (rule contentsI)
-  apply safe
-  apply (simp_all add: word_of_nat word_of_int_homs)
-   defer
-   apply (rule Rep_Integ_ne [THEN nonemptyE])
-   apply (rule bexI)
-    prefer 2
-    apply assumption
-   apply (auto simp add: RI_eq_diff)
+  apply (case_tac x rule: int_diff_cases)
+  apply (simp add: word_of_nat word_of_int_sub_hom)
   done
 
 lemma word_of_int_nat: