goals: simplified handling of implicit variables -- removed obsolete warning;

updated generated files;

cover 'schematic_lemma' etc.;

mark schematic statements explicitly;

eliminated spurious schematic statements;

explicit 'schematic_theorem' etc. for schematic theorem statements;

collapse category "schematic goal" in keyword table -- Proof General does not know about this;

added keyword category "schematic goal", which prevents any attempt to fork the proof;

merged

merged

separated instantiation of division_by_zero

epheremal replacement of field_simps by field_eq_simps; dropped old division_by_zero instance

adapted to new times_divide_eq simp situation

epheremal replacement of field_simps by field_eq_simps

dequalified fact name

sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit

separated instantiation of division_by_zero

dequalified fact name

less special treatment of times_divide_eq [simp]

sharpened constraint (c.f. 4e7f5b22dd7d)

more localization; tuned proofs

more localization; factored out lemmas for division_ring

modernized abstract algebra theories

merged

swapped generic code generator and SML code generator

removed obsolete Named_Thm_Set -- Named_Thms provides efficient member operation;

Item_Net/Named_Thms: export efficient member operation;

initialized atps reference with standard setup in the atp manager

compile

handle SPASS's equality predicate correctly in Isar proof reconstruction