author | wenzelm |
Mon, 13 Mar 2000 13:21:39 +0100 | |
changeset 8434 | 5e4bba59bfaa |
parent 7355 | 4c43090659ca |
child 8471 | 36446bf42b16 |
permissions | -rw-r--r-- |
4093 | 1 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset
|
2 |
theory FOL = IFOL |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset
|
3 |
files ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("FOL_lemmas2.ML"): |
4093 | 4 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset
|
5 |
axioms |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset
|
6 |
classical: "(~P ==> P) ==> P" |
4093 | 7 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset
|
8 |
use "FOL_lemmas1.ML" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset
|
9 |
use "cladata.ML" setup Cla.setup setup clasetup |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset
|
10 |
use "blastdata.ML" setup Blast.setup |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset
|
11 |
use "FOL_lemmas2.ML" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset
|
12 |
use "simpdata.ML" setup simpsetup setup Clasimp.setup |
4093 | 13 |
|
4854 | 14 |
end |