[isabelle] Convert an Isabelle term intro prenex normal form



Dear Isabelle experts,

I was wondering if there is a built-in Isabelle command to convert an Isabelle term into prenex normal form or anyone has ever developed similar procedures in Isabelle.

For example,

((!x::real. x*x>0) ∧ (?x::real. x=0))

should be able to be cast to something like

(?y::real. !x::real. x*x>0 ∧ y=0)

Many thanks,
Wenda

--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge




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