src/HOL/ROOT.ML

add formalization of a type of integers mod 2 to Library

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

use_thy "Main";
share_common_data ();
use_thy "Complex_Main";

val HOL_proofs = ! Proofterm.proofs;