author | immler |
Sun, 27 Oct 2019 21:51:14 -0400 | |
changeset 71035 | 6fe5a0e1fa8e |
parent 63167 | 0909deb8059b |
permissions | -rw-r--r-- |
29822 | 1 |
(* Title: HOL/Imperative_HOL/Imperative_HOL.thy |
26170 | 2 |
Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen |
3 |
*) |
|
4 |
||
63167 | 5 |
section \<open>Entry point into monadic imperative HOL\<close> |
26170 | 6 |
|
7 |
theory Imperative_HOL |
|
53109
186535065f5c
renamed theory Mrec to Legacy_Mrec, no longer included by default
krauss
parents:
37776
diff
changeset
|
8 |
imports Array Ref |
26170 | 9 |
begin |
10 |
||
11 |
end |