1
(* Title: HOL/IOA/ex/ROOT.ML
2
ID: $Id$
3
Author: Olaf Mueller
4
*)
5
6
time_use_thy "TrivEx";
7
time_use_thy "TrivEx2";