factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
combination of classical reasoner and simplifier auto_tac into Provers/clasimp.ML
explicitly introducing combined type clasimpset
FOL = IFOL +
rules
classical "(~P ==> P) ==> P"
end
ML val thy_data = [ClasetThyData.thy_data];