src/FOL/FOL.thy

added thin_refl to hyp_subst_tac

FOL = IFOL +

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

end

ML val thy_data = [ClasetThyData.thy_data];