paper about formalising parsing; seems to have done what we would like to do....probably also appears at ITP'11
theory Prelude
imports Main
begin
(*
To make the theory work under Isabelle 2009 and 2011
Isabelle 2009: set_ext
Isabelle 2011: set_eqI
*)
lemma set_eq_intro:
"(\<And>x. (x \<in> A) = (x \<in> B)) \<Longrightarrow> A = B"
by blast
end