681 lemmas star_of_eq_1 = star_of_eq [of _ 1, simplified star_of_one] |
681 lemmas star_of_eq_1 = star_of_eq [of _ 1, simplified star_of_one] |
682 |
682 |
683 text{*As above, for numerals*} |
683 text{*As above, for numerals*} |
684 |
684 |
685 lemmas star_of_number_less = |
685 lemmas star_of_number_less = |
686 star_of_less [of "number_of w", standard, simplified star_of_number_of] |
686 star_of_less [of "number_of w", simplified star_of_number_of] for w |
687 lemmas star_of_number_le = |
687 lemmas star_of_number_le = |
688 star_of_le [of "number_of w", standard, simplified star_of_number_of] |
688 star_of_le [of "number_of w", simplified star_of_number_of] for w |
689 lemmas star_of_number_eq = |
689 lemmas star_of_number_eq = |
690 star_of_eq [of "number_of w", standard, simplified star_of_number_of] |
690 star_of_eq [of "number_of w", simplified star_of_number_of] for w |
691 |
691 |
692 lemmas star_of_less_number = |
692 lemmas star_of_less_number = |
693 star_of_less [of _ "number_of w", standard, simplified star_of_number_of] |
693 star_of_less [of _ "number_of w", simplified star_of_number_of] for w |
694 lemmas star_of_le_number = |
694 lemmas star_of_le_number = |
695 star_of_le [of _ "number_of w", standard, simplified star_of_number_of] |
695 star_of_le [of _ "number_of w", simplified star_of_number_of] for w |
696 lemmas star_of_eq_number = |
696 lemmas star_of_eq_number = |
697 star_of_eq [of _ "number_of w", standard, simplified star_of_number_of] |
697 star_of_eq [of _ "number_of w", simplified star_of_number_of] for w |
698 |
698 |
699 lemmas star_of_simps [simp] = |
699 lemmas star_of_simps [simp] = |
700 star_of_add star_of_diff star_of_minus |
700 star_of_add star_of_diff star_of_minus |
701 star_of_mult star_of_divide star_of_inverse |
701 star_of_mult star_of_divide star_of_inverse |
702 star_of_div star_of_mod star_of_abs |
702 star_of_div star_of_mod star_of_abs |