changeset 26294 | c5fe289de634 |
parent 26086 | 3c243098b64a |
child 26514 | eff55c0a6d34 |
--- 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]