author | wenzelm |
Wed, 03 Nov 2010 21:53:56 +0100 | |
changeset 40335 | 3e4bb6e7c3ca |
parent 35762 | af3ff2ba4c54 |
permissions | -rw-r--r-- |
4905 | 1 |
(* Title: LCF/ex/ROOT.ML |
2 |
Author: Tobias Nipkow |
|
3 |
Copyright 1991 University of Cambridge |
|
4 |
||
15661
9ef583b08647
reverted renaming of Some/None in comments and strings;
wenzelm
parents:
15531
diff
changeset
|
5 |
Some examples from Lawrence Paulson's book Logic and Computation. |
4905 | 6 |
*) |
2820 | 7 |
|
24106 | 8 |
use_thys ["Ex1", "Ex2", "Ex3", "Ex4"]; |