src/HOL/ROOT.ML

corrected translation of integer operators,
keep argument order for n-ary symbols (conjunction, disjunction),
removed unused code

(* Classical Higher-order Logic -- batteries included *)

use_thys ["Complex_Main"];

val HOL_proofs = ! Proofterm.proofs;