tuned

--HG--
extra : rebase_source : 925e5859c312c4432ad0ce83c9f8a0714b599594

tuned

dropped dead code

isabelle update -u control_cartouches;

clarified specific use of inspect_contract: "any Bound variable will do" may render the term invalid for Term.fastype_of1 in inst_subst_tac (see also 7c3757fccf0e);

simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);

clarified context;

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;

renamed "pairself" to "apply2", in accordance to @{apply 2};

proper context;

proper context for match_tac etc.;

proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);

optional proof context for unify operations, for the sake of proper local options;

eliminated aliases;

modernized setup;

more uniform names;

Hypsubst preserves equality hypotheses

Fixes included for various theories affected by this change.

--HG--
extra : rebase_source : b0150e06a14c2821e03208834282be6eca87aae0

more qualified names;

tuned signature;

uniform Proof.context for hyp_subst_tac;

simplifier uses proper Proof.context instead of historic type simpset;

hyp_subst_tac allows to pass an optional simpset to the internal simplifier call to avoid renamed bound variable warnings in the simplifier call

Updated comment to reflect current state.

--HG--
extra : rebase_source : cca9fff2cbe5f8deae7a5d9b6aaf251a035993ed

discontinued old-style Term.list_abs in favour of plain Term.abs;

avoid stepping outside of context -- plain zero_var_indexes should be sufficient;

modernized some old-style infix operations, which were left over from the time of ML proof scripts;

misc tuning -- eliminated old-fashioned rep_thm;

renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;

modernized functor names;
tuned;

more direct Thm.cprem_of (with exception THM instead of Subscript);

eliminated old List.nth;
tuned;

more direct loose_bvar1;
tuned;

backed out my old attempt at single_hyp_subst_tac (67cd6ed76446)
It never was totally reliable, and better alternatives now exist (Subgoal.FOCUS).

use eta-contracted version for occurrence check (avoids possible non-termination)
Test case: lemma "fwrap f = (%v. f v) ==> P f" apply clarify;
pointed out by Thomas Sewell

less pervasive names from structure Thm;

proper context for mksimps etc. -- via simpset of the running Simplifier;

removed old CVS Ids;
tuned headers;

renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;

renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;

explicitly qualify Drule.standard;

simplified method setup;

unified type Proof.method and pervasive METHOD combinators;

meta_subst: xsymbols make it work with clean Pure;

single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp

inst_subst_tac: match types -- no longer assume that subst rule has exactly one type argument;
misc tuning -- more cterm operations, more qualified names;

Added function for computing instantiation for the subst rule, which is used
in vars_gen_hyp_subst_tac and blast_hyp_subst_tac to avoid problems with
HO unification.

blast_hyp_subst_tac: plain bool argument;

simplified method setup;

avoid handling of arbitrary exceptions;

simplified dest_eq;
do not export debuging stuff;
has_tvars: actually check all types within a term, not just its resulting type;
tuned;

slight type signature changes

fixed intendation

Name.is_bound;

setup: theory -> theory;

functor: no Simplifier argument;
Simplifier.theory_context;

Term.is_bound;

improved comments;

Deleted Library.option type.

the new subst tactic, by Lucas Dixon

fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions

- eliminated thin_leading_eqs_tac
- gen_hyp_subst_tac now uses asm_lr_simp_tac instead of asm_full_simp_tac,
in order to avoid divergence of new simplifier

'symmetric' attribute moved to Pure/calculation.ML;

use tracing function for trace output;

CHANGED_PROP;

tuned msg;

Method.SIMPLE_METHOD';

added 'symmetric' attribute;

added hypsubst;

added rev_eq_reflection;
export stac;
proof method setup: subst, hypsubst;

Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac

updated comment

added thin_refl to hyp_subst_tac

hyp_subst_tac checks if the equality has type variables and uses a suitable
method if so. Affects the dest_eq function

Removal of the tactical STATE

Prevent permutation of assumptions in hyp_subst_tac

Now uses rotate_tac and eta_contract_atom for greater speed

Removed a call to polymorphic mem

Replaced min by Int.min

Recoded with help from Toby to use rewriting instead of the
subst rule -- the latter was too slow. But it must resort to the subst rule
if the equality contains Vars.

Provers/hypsubst/REPEATN: deleted; using REPEAT_DETERM_N instead.

Provers/hypsubst: greatly simplified! No longer simulates a
"eres_inst_tac" using rev_cut_eq; instead simply rotates the chosen
equality to the end!

new comments explaining abandoned change

Updated refs to old Sign functions

Initial revision