renamed prove_raw to prove_internal; tuned;

merge/merge_refs: plain error instead of exception TERM;

Context positions.

added context_position.ML;

renamed Goal.prove_raw to Goal.prove_internal;

Method.Basic: include position;

tuned proofs: avoid implicit prems;

Basic text: include position; assumption/close: refer to non-atomic assumptions as well, implicit use of prems now considered legacy feature;

thm antiquotations

add lemma inj_of_nat

thm antiquotations

Unfortunately needed patch due to incompatibility with SML -- oo is infix and hence can not appear on the left handside of patterns

changed int stuff into integer for SMLNJ compatibility

more of_rat lemmas

add function of_rat and related lemmas

turned curry (op opr) into curry op opr --- because of smlnj

De-overloaded operations for int and real.

SML basis with type int representing proper integers, not machine words.

Tuned proofs : now use 'algebra ad: ...'

cooper_tac takes now two lists of theorems to be added/deleted from the simpset dor pre-simplification

changed val restriction to local due to smlnj

Changed normalizer Data to contain a simpset besides the list of instances; Before the method starts, it simplifies with this simpset; Added attribute 'algebra' to add and delete theorems from the simpset above;

Added algebra_tac; tuned;

Method now takes theorems to be added or deleted from a simpset for simplificatio before the core method starts

algebra_tac moved to file Tools/Groebner_Basis/groebner.ML; Method now takes theorems to be added or deleted from a simpset for simplificatio *before* the core method starts

nex example

Conversion for computation on constants now depends on the context

tuned setup for the fields instantiation for Groebner Bases;