equal
deleted
inserted
replaced
23 |
23 |
24 text "Unary minus works as for decimal numerals" |
24 text "Unary minus works as for decimal numerals" |
25 lemma "- 0x0A = - 10" by (rule refl) |
25 lemma "- 0x0A = - 10" by (rule refl) |
26 |
26 |
27 text \<open> |
27 text \<open> |
28 Hex and bin numerals are printed as decimal: @{term "0b10"} |
28 Hex and bin numerals are printed as decimal: \<^term>\<open>0b10\<close> |
29 \<close> |
29 \<close> |
30 term "0b10" |
30 term "0b10" |
31 term "0x0A" |
31 term "0x0A" |
32 |
32 |
33 text \<open> |
33 text \<open> |