equal
deleted
inserted
replaced
146 \noindent As figure \ref{fig:adaptation} illustrates, all these |
146 \noindent As figure \ref{fig:adaptation} illustrates, all these |
147 adaptation mechanisms have to act consistently; it is at the |
147 adaptation mechanisms have to act consistently; it is at the |
148 discretion of the user to take care for this. |
148 discretion of the user to take care for this. |
149 \<close> |
149 \<close> |
150 |
150 |
151 subsection \<open>Common adaptation applications\<close> |
151 subsection \<open>Common adaptation applications \label{sec:common_adaptation}\<close> |
152 |
152 |
153 text \<open> |
153 text \<open> |
154 The @{theory HOL} @{theory Main} theory already provides a code |
154 The @{theory HOL} @{theory Main} theory already provides a code |
155 generator setup which should be suitable for most applications. |
155 generator setup which should be suitable for most applications. |
156 Common extensions and modifications are available by certain |
156 Common extensions and modifications are available by certain |