(1) added axiom to ringb and theorems to enable algebra to prove the ideal membership problem; (2) Method algebra now calls algebra_tac which first tries to solve a universal formula, then in case of failure trie to solve the ideal membership problem (see HOL/Tools/Groebner_Basis/groebner.ML)

exported field_comp_conv: a numerical conversion over fields

dropped AxClass

tuned

Handle Subscript exception when looking up bound variables.

Added well-formedness check to Abst case in function prf_of.

added omission

bugfixes concerning strange theorems

fixed typo

const antiquotation clarified