# HG changeset patch
# User huffman
# Date 1330087043 -3600
# Node ID de514a98f6b63cfebdbe7d6c802faf4fcc26504a
# Parent  0abbf6dd09eeee5b83245566fc69ea03c5a03fc7
remove ill-formed lemmas word_pred_0_Min and word_m1_Min

diff -r 0abbf6dd09ee -r de514a98f6b6 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Fri Feb 24 13:33:03 2012 +0100
+++ b/src/HOL/Word/Word.thy	Fri Feb 24 13:37:23 2012 +0100
@@ -1200,12 +1200,6 @@
 lemma word_pred_0_n1: "word_pred 0 = word_of_int -1"
   unfolding word_pred_def uint_eq_0 pred_def by simp
 
-lemma word_pred_0_Min: "word_pred 0 = word_of_int Int.Min"
-  by (simp add: word_pred_0_n1 number_of_eq)
-
-lemma word_m1_Min: "- 1 = word_of_int Int.Min"
-  unfolding Min_def by (simp only: word_of_int_hom_syms)
-
 lemma succ_pred_no [simp]:
   "word_succ (number_of bin) = number_of (Int.succ bin) & 
     word_pred (number_of bin) = number_of (Int.pred bin)"