equal
deleted
inserted
replaced
1 |
1 |
2 FOL = IFOL + |
2 theory FOL = IFOL |
|
3 files ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("FOL_lemmas2.ML"): |
3 |
4 |
4 rules |
5 axioms |
5 classical "(~P ==> P) ==> P" |
6 classical: "(~P ==> P) ==> P" |
6 |
7 |
7 setup ClasetThyData.setup |
8 use "FOL_lemmas1.ML" |
8 setup attrib_setup (* FIXME move to IFOL.thy *) |
9 use "cladata.ML" setup Cla.setup setup clasetup |
|
10 use "blastdata.ML" setup Blast.setup |
|
11 use "FOL_lemmas2.ML" |
|
12 use "simpdata.ML" setup simpsetup setup Clasimp.setup |
9 |
13 |
10 end |
14 end |