# HG changeset patch
# User kleing
# Date 1205734540 -3600
# Node ID c5fe289de63421d95085e6755a0351a6722fbfe9
# Parent  a71ea4a57f446c29cc60cd75fb800a1ff17b0cd6
fixed broken bintrunc lemma

diff -r a71ea4a57f44 -r c5fe289de634 src/HOL/Word/BinGeneral.thy
--- a/src/HOL/Word/BinGeneral.thy	Sat Mar 15 22:40:41 2008 +0100
+++ b/src/HOL/Word/BinGeneral.thy	Mon Mar 17 07:15:40 2008 +0100
@@ -459,7 +459,8 @@
   by auto
 
 lemmas bintrunc_Suc_Ialts = 
-  bintrunc_Min_I bintrunc_BIT_I [THEN bintrunc_Suc_lem, standard]
+  bintrunc_Min_I [THEN bintrunc_Suc_lem, standard]
+  bintrunc_BIT_I [THEN bintrunc_Suc_lem, standard]
 
 lemmas sbintrunc_BIT_I = trans [OF sbintrunc_Suc_BIT thobini1]