src/HOL/String.thy
changeset 60758 d8d85a8172b5
parent 59631 34030d67afb9
child 60801 7664e0916eec
     1.1 --- a/src/HOL/String.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/String.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -1,12 +1,12 @@
     1.4  (* Author: Tobias Nipkow, Florian Haftmann, TU Muenchen *)
     1.5  
     1.6 -section {* Character and string types *}
     1.7 +section \<open>Character and string types\<close>
     1.8  
     1.9  theory String
    1.10  imports Enum
    1.11  begin
    1.12  
    1.13 -subsection {* Characters and strings *}
    1.14 +subsection \<open>Characters and strings\<close>
    1.15  
    1.16  datatype nibble =
    1.17      Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
    1.18 @@ -246,7 +246,7 @@
    1.19    "nat_of_char (Char x y) = nat_of_nibble x * 16 + nat_of_nibble y"
    1.20    by (simp add: nat_of_char_def)
    1.21  
    1.22 -setup {*
    1.23 +setup \<open>
    1.24  let
    1.25    val nibbles = map_range (Thm.cterm_of @{context} o HOLogic.mk_nibble) 16;
    1.26    val simpset =
    1.27 @@ -261,7 +261,7 @@
    1.28      [((@{binding nat_of_char_simps}, []), [(code_eqns, [])])]
    1.29    #> snd
    1.30  end
    1.31 -*}
    1.32 +\<close>
    1.33  
    1.34  declare nat_of_char_simps [code]
    1.35  
    1.36 @@ -281,7 +281,7 @@
    1.37    with Char show ?thesis by (simp add: nat_of_char_def add.commute)
    1.38  qed
    1.39  
    1.40 -code_datatype Char -- {* drop case certificate for char *}
    1.41 +code_datatype Char -- \<open>drop case certificate for char\<close>
    1.42  
    1.43  lemma case_char_code [code]:
    1.44    "case_char f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
    1.45 @@ -354,7 +354,7 @@
    1.46  qed
    1.47  
    1.48  
    1.49 -subsection {* Strings as dedicated type *}
    1.50 +subsection \<open>Strings as dedicated type\<close>
    1.51  
    1.52  typedef literal = "UNIV :: string set"
    1.53    morphisms explode STR ..
    1.54 @@ -399,7 +399,7 @@
    1.55  lifting_update literal.lifting
    1.56  lifting_forget literal.lifting
    1.57  
    1.58 -subsection {* Code generator *}
    1.59 +subsection \<open>Code generator\<close>
    1.60  
    1.61  ML_file "Tools/string_code.ML"
    1.62  
    1.63 @@ -414,9 +414,9 @@
    1.64      and (Haskell) "String"
    1.65      and (Scala) "String"
    1.66  
    1.67 -setup {*
    1.68 +setup \<open>
    1.69    fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
    1.70 -*}
    1.71 +\<close>
    1.72  
    1.73  code_printing
    1.74    class_instance literal :: equal \<rightharpoonup>
    1.75 @@ -427,7 +427,7 @@
    1.76      and (Haskell) infix 4 "=="
    1.77      and (Scala) infixl 5 "=="
    1.78  
    1.79 -setup {* Sign.map_naming (Name_Space.mandatory_path "Code") *}
    1.80 +setup \<open>Sign.map_naming (Name_Space.mandatory_path "Code")\<close>
    1.81  
    1.82  definition abort :: "literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.83  where [simp, code del]: "abort _ f = f ()"
    1.84 @@ -435,9 +435,9 @@
    1.85  lemma abort_cong: "msg = msg' ==> Code.abort msg f = Code.abort msg' f"
    1.86  by simp
    1.87  
    1.88 -setup {* Sign.map_naming Name_Space.parent_path *}
    1.89 +setup \<open>Sign.map_naming Name_Space.parent_path\<close>
    1.90  
    1.91 -setup {* Code_Simp.map_ss (Simplifier.add_cong @{thm Code.abort_cong}) *}
    1.92 +setup \<open>Code_Simp.map_ss (Simplifier.add_cong @{thm Code.abort_cong})\<close>
    1.93  
    1.94  code_printing constant Code.abort \<rightharpoonup>
    1.95      (SML) "!(raise/ Fail/ _)"