do not open OldGoals;

renamed functor SplitterFun to Splitter, require explicit theory;

renamed functor BlastFun to Blast, require explicit theory; eliminated src/FOL/blastdata.ML;

eliminated OldGoals.prove_goal;

explicit OldGoals;

structure OldGoals: no pervasive names;

renamed functor ProjectRuleFun to Project_Rule; renamed structure ProjectRule to Project_Rule;

renamed functor InductFun to Induct;

tuned;

renamed Pure/tctical.ML to Pure/tactical.ML;

eliminated print_goals_without_context -- proper pretty printing;

Display_Goal.pretty_goals: always Markup.subgoal, clarified options;

removed Formal_Power_Series_Examples (cf. adea7a729c7a);

make: keep going by default;

merged

merged

fixed proof --- fact_setprod removed for fact_altdef_nat

merged

Vandermonde vs Pochhammer; Hypergeometric series - very basic facts

More theorems about pochhammer

Moved theorem binomial_symmetric from Formal_Power_Series to here

Moved important theorems from FPS_Examples to FPS --- they are not really examples but useful theorems that are being reproved since unnoticed.

removed obsolete ML proof tools;

more @{theory} antiquotations;

eliminated adhoc ML code;

misc modernization: proper method setup instead of adhoc ML proofs;

global_claset_of;

Proper context for simpset_of, claset_of, clasimpset_of.

local simpset_of;

renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;