> I am curious -- how easy is it to use theoremquest for playing with > equational theories? Let me turn the question around: How easy is it to play with equational theories in HOL Light? Because this is the planed basis for TheoremQuest. -Tom