split preparing clauses and writing problemfile;
included results of count_constants in return-type of prover;
optionally pass counted constants to prover;
removed unused external_prover from signature
(* 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