src/Doc/Codegen/Adaptation.thy
changeset 63680 6e1e8b5abbfa
parent 63669 256fc20716f2
child 65041 2525e680f94f
     1.1 --- a/src/Doc/Codegen/Adaptation.thy	Fri Aug 12 17:49:02 2016 +0200
     1.2 +++ b/src/Doc/Codegen/Adaptation.thy	Fri Aug 12 17:53:55 2016 +0200
     1.3 @@ -154,7 +154,7 @@
     1.4    The @{theory HOL} @{theory Main} theory already provides a code
     1.5    generator setup which should be suitable for most applications.
     1.6    Common extensions and modifications are available by certain
     1.7 -  theories in @{dir "~~/src/HOL/Library"}; beside being useful in
     1.8 +  theories in \<^dir>\<open>~~/src/HOL/Library\<close>; beside being useful in
     1.9    applications, they may serve as a tutorial for customising the code
    1.10    generator setup (see below \secref{sec:adaptation_mechanisms}).
    1.11