--- a/src/HOL/ex/Hex_Bin_Examples.thy Tue Oct 06 17:46:07 2015 +0200
+++ b/src/HOL/ex/Hex_Bin_Examples.thy Tue Oct 06 17:47:28 2015 +0200
@@ -2,7 +2,7 @@
Author: Gerwin Klein, NICTA
*)
-section {* Examples for hexadecimal and binary numerals *}
+section \<open>Examples for hexadecimal and binary numerals\<close>
theory Hex_Bin_Examples imports Main
begin
@@ -12,10 +12,10 @@
lemma "0xFF = 255" by (rule refl)
lemma "0xF = 0b1111" by (rule refl)
-text {*
+text \<open>
Just like decimal numeral they are polymorphic, for arithmetic
they need to be constrained
-*}
+\<close>
lemma "0x0A + 0x10 = (0x1A :: nat)" by simp
text "The number of leading zeros is irrelevant"
@@ -24,17 +24,17 @@
text "Unary minus works as for decimal numerals"
lemma "- 0x0A = - 10" by (rule refl)
-text {*
+text \<open>
Hex and bin numerals are printed as decimal: @{term "0b10"}
-*}
+\<close>
term "0b10"
term "0x0A"
-text {*
+text \<open>
The numerals 0 and 1 are syntactically different from the
constants 0 and 1. For the usual numeric types, their values
are the same, though.
-*}
+\<close>
lemma "0x01 = 1" oops
lemma "0x00 = 0" oops