prefer qualified names;

updated to infer_instantiate;

Thm.cterm_of and Thm.ctyp_of operate on local context;

tuned signature -- prefer qualified names;

proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;

eliminated aliases;

dropped dead code

--HG--
extra : rebase_source : 7dc118a82fd6b8aeb0b217eab0f907eab6354467

more robust exception pattern General.Subscript;

eliminated old List.nth;
tuned;

modernized structure Proof_Context;

tuned titles

farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)

Fixed bug that caused (r)trancl_tac to crash when the term denoting the relation
contained variables bound by meta level quantifiers.

map_range (and map_index) combinator

tuned;

explicit indication of Unsynchronized.ref;

trancl_tac etc.: back to static context -- problem was caused by bad solver in AFP/JiveDataStoreModel;

qualified Subgoal.FOCUS;

trans_tac: use theory from goal state, not the static context, which seems to be outdated under certain circumstances (why?);

replaced old METAHYPS by FOCUS;
eliminated homegrown SUBGOAL combinator -- beware of exception Subscript in body;
modernized functor names;
minimal tuning of sources;
reactivated dead quasi.ML (ever used?);

Merge.

use long names for old-style fold combinators;

Terms returned by decomp are now eta-contracted.

"prove" function now instantiates relation variable in order
to avoid problems with higher-order unification. This allows
relations to be encoded as binary predicates.

Removed practically all references to Library.foldr.

Move towards standard functions.

Deleted Library.option type.

Documentation added/improved.

*** empty log message ***

New prover for transitive and reflexive-transitive closure of relations.
- Code in Provers/trancl.ML
- HOL: Simplifier set up to use it as solver