src/HOL/Imperative_HOL/Imperative_HOL_ex.thy
author haftmann
Tue, 30 Jun 2009 14:53:58 +0200
changeset 31872 a564aca741f2
parent 30694 4b182a031731
child 34051 1a82e2e29d67
permissions -rw-r--r--
tuned

(*  Title:      HOL/Imperative_HOL/Imperative_HOL_ex.thy
    Author:     John Matthews, Galois Connections;
                Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
*)

header {* Monadic imperative HOL with examples *}

theory Imperative_HOL_ex
imports Imperative_HOL "ex/Imperative_Quicksort"
begin

end