equal
deleted
inserted
replaced
538 |
538 |
539 lemma of_nat_numeral [simp]: "of_nat (numeral n) = numeral n" |
539 lemma of_nat_numeral [simp]: "of_nat (numeral n) = numeral n" |
540 by (induct n) (simp_all only: numeral.simps numeral_class.numeral.simps of_nat_add of_nat_1) |
540 by (induct n) (simp_all only: numeral.simps numeral_class.numeral.simps of_nat_add of_nat_1) |
541 |
541 |
542 lemma numeral_unfold_funpow: |
542 lemma numeral_unfold_funpow: |
543 "numeral k = (op + 1 ^^ numeral k) 0" |
543 "numeral k = ((+) 1 ^^ numeral k) 0" |
544 unfolding of_nat_def [symmetric] by simp |
544 unfolding of_nat_def [symmetric] by simp |
545 |
545 |
546 end |
546 end |
547 |
547 |
548 lemma transfer_rule_numeral: |
548 lemma transfer_rule_numeral: |