replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style
(* Title: HOL/Extraction/ROOT.ML
ID: $Id$
Examples for program extraction in Higher-Order Logic.
*)
if HOL_proofs < 2 then
warning "HOL proof terms required for running extraction examples"
else
(proofs := 2;
time_use_thy "QuotRem";
time_use_thy "Warshall";
time_use_thy "Higman");