author | wenzelm |
Wed, 26 Mar 2008 22:38:55 +0100 | |
changeset 26408 | 6964c4799f47 |
parent 26322 | eaf634e975fa |
child 35762 | af3ff2ba4c54 |
permissions | -rw-r--r-- |
17480 | 1 |
(* Title: FOLP/ex/ROOT.ML |
0 | 2 |
ID: $Id$ |
1459 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1992 University of Cambridge |
5 |
||
17480 | 6 |
Examples for First-Order Logic. |
0 | 7 |
*) |
8 |
||
25991 | 9 |
use_thys [ |
10 |
"Intro", |
|
11 |
"Nat", |
|
12 |
"Foundation", |
|
26322 | 13 |
"If", |
14 |
"Intuitionistic", |
|
26408 | 15 |
"Classical", |
16 |
"Propositional_Int", |
|
17 |
"Quantifiers_Int", |
|
18 |
"Propositional_Cla", |
|
19 |
"Quantifiers_Cla" |
|
25991 | 20 |
]; |