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)
use "../settings.ML";no_document use_thy "While_Combinator";use_thy "simp";use_thy "WFrec";use_thy "Partial";