Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
distributed them over Real/ (to do with bijections and density).
Library/NatPair became Nat_Int_Bij and made that part of Main.
(* Title: HOL/Main.thy
ID: $Id$
*)
header {* Main HOL *}
theory Main
imports Plain Map Nat_Int_Bij Recdef
begin
ML {* val HOL_proofs = ! Proofterm.proofs *}
text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
end