src/FOL/FOL.thy

hyp_subst_tac checks if the equality has type variables and uses a suitable
method if so. Affects the dest_eq function

FOL = IFOL +

rules
  classical "(~P ==> P) ==> P"

end

ML val thy_data = [ClasetThyData.thy_data];