equal
deleted
inserted
replaced
455 (* although bintrunc_minus_simps, if added to default simpset, |
455 (* although bintrunc_minus_simps, if added to default simpset, |
456 tends to get applied where it's not wanted in developing the theories, |
456 tends to get applied where it's not wanted in developing the theories, |
457 we get a version for when the word length is given literally *) |
457 we get a version for when the word length is given literally *) |
458 |
458 |
459 lemmas nat_non0_gr = |
459 lemmas nat_non0_gr = |
460 trans [OF iszero_def [THEN Not_eq_iff [THEN iffD2]] neq0_conv, standard] |
460 trans [OF iszero_def [THEN Not_eq_iff [THEN iffD2]] refl, standard] |
461 |
461 |
462 lemmas bintrunc_pred_simps [simp] = |
462 lemmas bintrunc_pred_simps [simp] = |
463 bintrunc_minus_simps [of "number_of bin", simplified nobm1, standard] |
463 bintrunc_minus_simps [of "number_of bin", simplified nobm1, standard] |
464 |
464 |
465 lemmas sbintrunc_pred_simps [simp] = |
465 lemmas sbintrunc_pred_simps [simp] = |