src/HOL/Library/Code_Char.thy
changeset 60500 903bb1495239
parent 58881 b9556a055632
child 61076 bdc1e2f0a86a
     1.1 --- a/src/HOL/Library/Code_Char.thy	Wed Jun 17 10:57:11 2015 +0200
     1.2 +++ b/src/HOL/Library/Code_Char.thy	Wed Jun 17 11:03:05 2015 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Florian Haftmann
     1.5  *)
     1.6  
     1.7 -section {* Code generation of pretty characters (and strings) *}
     1.8 +section \<open>Code generation of pretty characters (and strings)\<close>
     1.9  
    1.10  theory Code_Char
    1.11  imports Main Char_ord
    1.12 @@ -15,10 +15,10 @@
    1.13      and (Haskell) "Prelude.Char"
    1.14      and (Scala) "Char"
    1.15  
    1.16 -setup {*
    1.17 +setup \<open>
    1.18    fold String_Code.add_literal_char ["SML", "OCaml", "Haskell", "Scala"] 
    1.19    #> String_Code.add_literal_list_string "Haskell"
    1.20 -*}
    1.21 +\<close>
    1.22  
    1.23  code_printing
    1.24    class_instance char :: equal \<rightharpoonup>
    1.25 @@ -107,9 +107,9 @@
    1.26  |  constant "Orderings.less_eq :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
    1.27      (SML) "!((_ : string) <= _)"
    1.28      and (OCaml) "!((_ : string) <= _)"
    1.29 -    -- {* Order operations for @{typ String.literal} work in Haskell only 
    1.30 +    -- \<open>Order operations for @{typ String.literal} work in Haskell only 
    1.31            if no type class instance needs to be generated, because String = [Char] in Haskell
    1.32 -          and @{typ "char list"} need not have the same order as @{typ String.literal}. *}
    1.33 +          and @{typ "char list"} need not have the same order as @{typ String.literal}.\<close>
    1.34      and (Haskell) infix 4 "<="
    1.35      and (Scala) infixl 4 "<="
    1.36      and (Eval) infixl 6 "<="