define copy functions using combinators; add checking for failed proofs of induction rules
(* Title: HOL/Imperative_HOL/Imperative_HOL_ex.thy
Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
*)
header {* Mmonadic imperative HOL with examples *}
theory Imperative_HOL_ex
imports Imperative_HOL "ex/Imperative_Quicksort"
begin
end