# HG changeset patch
# User haftmann
# Date 1531939876 -7200
# Node ID 81639cc48d0a7c98d7f874b45087b2b8043ba040
# Parent  5a5146c3a35b773d32266f09cd069c071ddb66cc
more cartouches

diff -r 5a5146c3a35b -r 81639cc48d0a src/HOL/Library/IArray.thy
--- a/src/HOL/Library/IArray.thy	Thu Jul 19 09:22:32 2018 +0100
+++ b/src/HOL/Library/IArray.thy	Wed Jul 18 20:51:16 2018 +0200
@@ -1,4 +1,4 @@
-section "Immutable Arrays with Code Generation"
+section \<open>Immutable Arrays with Code Generation\<close>
 
 theory IArray
 imports Main
@@ -43,7 +43,7 @@
 end
 
 
-subsection "Code Generation"
+subsection \<open>Code Generation\<close>
 
 code_reserved SML Vector