major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
Ref System Logics HOL ZF Inductive AxClass TutorialI IsarOverview IsarRef Exercises Locales