author | blanchet |
Wed, 14 Apr 2010 17:10:16 +0200 | |
changeset 36141 | c31602d268be |
parent 35762 | af3ff2ba4c54 |
permissions | -rw-r--r-- |
17480 | 1 |
(* Title: FOLP/ex/ROOT.ML |
1459 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 3 |
Copyright 1992 University of Cambridge |
4 |
||
17480 | 5 |
Examples for First-Order Logic. |
0 | 6 |
*) |
7 |
||
25991 | 8 |
use_thys [ |
9 |
"Intro", |
|
10 |
"Nat", |
|
11 |
"Foundation", |
|
26322 | 12 |
"If", |
13 |
"Intuitionistic", |
|
26408 | 14 |
"Classical", |
15 |
"Propositional_Int", |
|
16 |
"Quantifiers_Int", |
|
17 |
"Propositional_Cla", |
|
18 |
"Quantifiers_Cla" |
|
25991 | 19 |
]; |