src/HOL/String.thy
changeset 61799 4cf66f21b764
parent 61348 d7215449be83
child 62364 9209770bdcdf
     1.1 --- a/src/HOL/String.thy	Mon Dec 07 10:23:50 2015 +0100
     1.2 +++ b/src/HOL/String.thy	Mon Dec 07 10:38:04 2015 +0100
     1.3 @@ -115,7 +115,7 @@
     1.4    by (simp add: nibble_of_nat_def)
     1.5  
     1.6  datatype char = Char nibble nibble
     1.7 -  -- "Note: canonical order of character encoding coincides with standard term ordering"
     1.8 +  \<comment> "Note: canonical order of character encoding coincides with standard term ordering"
     1.9  
    1.10  syntax
    1.11    "_Char" :: "str_position => char"    ("CHR _")
    1.12 @@ -281,7 +281,7 @@
    1.13    with Char show ?thesis by (simp add: nat_of_char_def add.commute)
    1.14  qed
    1.15  
    1.16 -code_datatype Char -- \<open>drop case certificate for char\<close>
    1.17 +code_datatype Char \<comment> \<open>drop case certificate for char\<close>
    1.18  
    1.19  lemma case_char_code [code]:
    1.20    "case_char f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"