src/FOL/FOL.thy
author wenzelm
Wed, 25 Aug 1999 20:45:19 +0200
changeset 7355 4c43090659ca
parent 5887 0864c6578d16
child 8471 36446bf42b16
permissions -rw-r--r--
proper bootstrap of IFOL/FOL theories and packages;


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 Clasimp.setup

end