author | wenzelm |
Fri, 08 May 1998 13:54:45 +0200 | |
changeset 4905 | be73ddff6c5a |
parent 4446 | 097004a470fb |
child 6349 | f7750d816c21 |
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 |
LCF_build_completed; (*Cause examples to fail if LCF did*) |
|
11 |
||
4446 | 12 |
set proof_timing; |
2820 | 13 |
|
4905 | 14 |
use_thy "Ex1"; |
15 |
use_thy "Ex2"; |
|
16 |
use_thy "Ex3"; |
|
17 |
use_thy "Ex4"; |