author bulwahn
Thu, 10 Dec 2009 11:58:26 +0100
changeset 34051 1a82e2e29d67
parent 31872 a564aca741f2
child 36098 53992c639da5
permissions -rw-r--r--
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas

(*  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" "ex/Imperative_Reverse" "ex/Linked_Lists"