author | wenzelm |
Wed, 15 Mar 2000 18:42:13 +0100 | |
changeset 8471 | 36446bf42b16 |
parent 7355 | 4c43090659ca |
child 8643 | 331f0c75e3dc |
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" |
8471 | 9 |
use "cladata.ML" setup Cla.setup setup clasetup |
10 |
use "blastdata.ML" setup Blast.setup |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset
|
11 |
use "FOL_lemmas2.ML" |
8471 | 12 |
use "simpdata.ML" setup simpsetup |
13 |
setup "Simplifier.method_setup Splitter.split_modifiers" |
|
14 |
setup Splitter.setup setup Clasimp.setup |
|
4093 | 15 |
|
4854 | 16 |
end |