changeset 47487 | 54a2f155621b |
parent 47400 | b7625245a846 |
child 47819 | d402ac2288b8 |
47486:4d49f3ffe97e | 47487:54a2f155621b |
---|---|
733 lemma [code abstract]: |
733 lemma [code abstract]: |
734 "Target_Numeral.of_nat (nat k) = max 0 (Target_Numeral.of_int k)" |
734 "Target_Numeral.of_nat (nat k) = max 0 (Target_Numeral.of_int k)" |
735 by (simp add: of_nat_def of_int_of_nat max_def) |
735 by (simp add: of_nat_def of_int_of_nat max_def) |
736 |
736 |
737 end |
737 end |
738 |