1
(* Title: LCF/ex/ROOT.ML
2
ID: $Id$
3
Author: Tobias Nipkow
4
Copyright 1991 University of Cambridge
5
6
Some examples from Lawrence Paulson's book Logic and Computation.
7
*)
8
9
time_use_thy "Ex1";
10
time_use_thy "Ex2";
11
time_use_thy "Ex3";
12
time_use_thy "Ex4";