src/HOL/HOL.ML

 
 end;
 
 
 
-(*** Load simpdata.ML to be able to initialize HOL's simpset ***)
+(*** Setting up the classical reasoner and simplifier ***)
 
 
 (** Applying HypsubstFun to generate hyp_subst_tac **)
 section "Classical Reasoner";