src/CTT/Main.thy

correctly handle TFrees that occur in (local) facts -- Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"

header {* Main includes everything *}

theory Main
imports CTT Arith Bool
begin
end