equal
deleted
inserted
replaced
1 (* Title: HOL/Imperative_HOL/Imperative_HOL_ex.thy |
1 (* Title: HOL/Imperative_HOL/Imperative_HOL_ex.thy |
2 Author: John Matthews, Galois Connections; |
2 Author: John Matthews, Galois Connections; |
3 Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen |
3 Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 header {* Monadic imperative HOL with examples *} |
6 section {* Monadic imperative HOL with examples *} |
7 |
7 |
8 theory Imperative_HOL_ex |
8 theory Imperative_HOL_ex |
9 imports Imperative_HOL Overview |
9 imports Imperative_HOL Overview |
10 "ex/Imperative_Quicksort" "ex/Imperative_Reverse" "ex/Linked_Lists" "ex/SatChecker" |
10 "ex/Imperative_Quicksort" "ex/Imperative_Reverse" "ex/Linked_Lists" "ex/SatChecker" |
11 Legacy_Mrec |
11 Legacy_Mrec |