equal
deleted
inserted
replaced
|
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 *) |
1 |
8 |
2 writeln"Root file for LCF examples"; |
9 writeln"Root file for LCF examples"; |
3 LCF_build_completed; (*Cause examples to fail if LCF did*) |
10 LCF_build_completed; (*Cause examples to fail if LCF did*) |
4 |
11 |
5 set proof_timing; |
12 set proof_timing; |
6 |
13 |
7 use "ex.ML"; |
14 use_thy "Ex1"; |
|
15 use_thy "Ex2"; |
|
16 use_thy "Ex3"; |
|
17 use_thy "Ex4"; |