author | wenzelm |
Fri, 31 Mar 2000 22:22:23 +0200 | |
changeset 8643 | 331f0c75e3dc |
parent 8471 | 36446bf42b16 |
child 9487 | 7e377f912629 |
permissions | -rw-r--r-- |
theory FOL = IFOL files ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("FOL_lemmas2.ML"): axioms classical: "(~P ==> P) ==> P" use "FOL_lemmas1.ML" use "cladata.ML" setup Cla.setup setup clasetup use "blastdata.ML" setup Blast.setup use "FOL_lemmas2.ML" use "simpdata.ML" setup simpsetup setup cong_attrib_setup setup "Simplifier.method_setup Splitter.split_modifiers" setup Splitter.setup setup Clasimp.setup end