author | wenzelm |
Mon, 02 Aug 1999 15:39:23 +0200 | |
changeset 7149 | d0c2168f7704 |
parent 6349 | f7750d816c21 |
child 9000 | c20d58286a51 |
permissions | -rw-r--r-- |
4905 | 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 |
*) |
|
2820 | 8 |
|
9 |
writeln"Root file for LCF examples"; |
|
10 |
||
4446 | 11 |
set proof_timing; |
4905 | 12 |
use_thy "Ex1"; |
13 |
use_thy "Ex2"; |
|
14 |
use_thy "Ex3"; |
|
15 |
use_thy "Ex4"; |