src/HOL/Library/Char_ord.thy
changeset 60500 903bb1495239
parent 58881 b9556a055632
child 60679 ade12ef2773c
     1.1 --- a/src/HOL/Library/Char_ord.thy	Wed Jun 17 10:57:11 2015 +0200
     1.2 +++ b/src/HOL/Library/Char_ord.thy	Wed Jun 17 11:03:05 2015 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Norbert Voelker, Florian Haftmann
     1.5  *)
     1.6  
     1.7 -section {* Order on characters *}
     1.8 +section \<open>Order on characters\<close>
     1.9  
    1.10  theory Char_ord
    1.11  imports Main
    1.12 @@ -123,7 +123,7 @@
    1.13  lifting_update literal.lifting
    1.14  lifting_forget literal.lifting
    1.15  
    1.16 -text {* Legacy aliasses *}
    1.17 +text \<open>Legacy aliasses\<close>
    1.18  
    1.19  lemmas nibble_less_eq_def = less_eq_nibble_def
    1.20  lemmas nibble_less_def = less_nibble_def