[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 Li
PhD Candidate
Computer Laboratory
University of Cambridge

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