renamed former Int.int_induct to Int.int_of_nat_induct, former Presburger.int_induct to Int.int_induct: is more conservative and more natural than the intermediate solution
(* Title: HOL/Quotient_Examples/ROOT.ML
Author: Cezary Kaliszyk and Christian Urban
Testing the quotient package.
*)
use_thys ["FSet", "Quotient_Int", "Quotient_Message"];