author | wenzelm |
Sat, 26 Jun 2021 20:55:43 +0200 | |
changeset 73884 | 0a12ca4f3e8d |
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 |