| author | haftmann |
| Tue, 22 Apr 2008 08:33:23 +0200 | |
| changeset 26736 | e6091328718f |
| parent 26408 | 6964c4799f47 |
| 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 |
]; |