equal
deleted
inserted
replaced
22 *}(*>*) |
22 *}(*>*) |
23 |
23 |
24 text {* |
24 text {* |
25 @{text "Imperative HOL"} is a leightweight framework for reasoning |
25 @{text "Imperative HOL"} is a leightweight framework for reasoning |
26 about imperative data structures in @{text "Isabelle/HOL"} |
26 about imperative data structures in @{text "Isabelle/HOL"} |
27 \cite{Nipkow-et-al:2002:tutorial}. Its basic ideas are described in |
27 @{cite "Nipkow-et-al:2002:tutorial"}. Its basic ideas are described in |
28 \cite{Bulwahn-et-al:2008:imp_HOL}. However their concrete |
28 @{cite "Bulwahn-et-al:2008:imp_HOL"}. However their concrete |
29 realisation has changed since, due to both extensions and |
29 realisation has changed since, due to both extensions and |
30 refinements. Therefore this overview wants to present the framework |
30 refinements. Therefore this overview wants to present the framework |
31 \qt{as it is} by now. It focusses on the user-view, less on matters |
31 \qt{as it is} by now. It focusses on the user-view, less on matters |
32 of construction. For details study of the theory sources is |
32 of construction. For details study of the theory sources is |
33 encouraged. |
33 encouraged. |