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