Reimplemented algebra method; now controlled by attribute.
(* Title: LCF/ex/ROOT.ML
ID: $Id$
Author: Tobias Nipkow
Copyright 1991 University of Cambridge
Some examples from Lawrence Paulson's book Logic and Computation.
*)
time_use_thy "Ex1";
time_use_thy "Ex2";
time_use_thy "Ex3";
time_use_thy "Ex4";