src/HOL/Library/IArray.thy
changeset 68654 81639cc48d0a
parent 67613 ce654b0e6d69
child 68655 90652333fae2
     1.1 --- a/src/HOL/Library/IArray.thy	Thu Feb 15 12:11:00 2018 +0100
     1.2 +++ b/src/HOL/Library/IArray.thy	Wed Jul 18 20:51:16 2018 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -section "Immutable Arrays with Code Generation"
     1.5 +section \<open>Immutable Arrays with Code Generation\<close>
     1.6  
     1.7  theory IArray
     1.8  imports Main
     1.9 @@ -43,7 +43,7 @@
    1.10  end
    1.11  
    1.12  
    1.13 -subsection "Code Generation"
    1.14 +subsection \<open>Code Generation\<close>
    1.15  
    1.16  code_reserved SML Vector
    1.17