# [isabelle] local datatypes?

Hello,
Is it possible to introduce a new datatype that scoped only for the duration of a single proof? My datatype doesn't technically *depend* on local definitions inside the proof -- I just want to make it clear to the reader that these datatype only needs to be understood in the context of this proof.
That is, I want to write something like this:
theorem soundness:
"\<forall> a :: A. prov a --> sem a"
proof
datatype myNewType = Foo int | Bar nat
fun f :: "A => myNewType => bool"
where (* ... *)
lemma soundness_first_step:
"\<forall> a. prov a --> (\<exists> m. f a m)"
proof (* ... *) qed
lemma soundness_second_step:
"\<forall> a. (\<exists> m. f a m) --> sem a"
proof (* ... *) qed
show ?thesis
using soundness_first_step
and soundness_second_step by auto
qed
Thanks very much,
john

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*