author | haftmann |
Sun, 18 Jan 2009 21:12:06 +0100 | |
changeset 29554 | 7e5e5ebb7bf7 |
parent 24106 | f2965bf954dc |
child 35762 | af3ff2ba4c54 |
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 |
||
15661
9ef583b08647
reverted renaming of Some/None in comments and strings;
wenzelm
parents:
15531
diff
changeset
|
6 |
Some examples from Lawrence Paulson's book Logic and Computation. |
4905 | 7 |
*) |
2820 | 8 |
|
24106 | 9 |
use_thys ["Ex1", "Ex2", "Ex3", "Ex4"]; |