replaced read_term_legacy by read_prop_legacy;
read: intern_skolem before type-inference (many workarounds!);
read: reject_tvars;
removed obsolete TypeInfer.logicT -- use dummyT;
add_fixes: not constraints for external names;
(* $Id$ *)
header {* Main includes everything *}
theory Main
imports CTT Arith Bool
begin
end