#
a8efb54f |
|
26-Jan-2020 |
haftmann <none@none> |
tuned --HG-- extra : rebase_source : 925e5859c312c4432ad0ce83c9f8a0714b599594
|
#
a2ee90ec |
|
22-Jan-2020 |
haftmann <none@none> |
tuned
|
#
3f031650 |
|
22-Jan-2020 |
haftmann <none@none> |
dropped dead code
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
12f8899f |
|
09-Jul-2015 |
wenzelm <none@none> |
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);
|
#
9a9cf694 |
|
05-Jul-2015 |
wenzelm <none@none> |
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
|
#
65c57129 |
|
06-Mar-2015 |
wenzelm <none@none> |
clarified context;
|
#
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
#
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
#
b8d56fe6 |
|
10-Feb-2015 |
wenzelm <none@none> |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
|
#
13ddea91 |
|
26-Nov-2014 |
wenzelm <none@none> |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
#
b6ee6a20 |
|
09-Nov-2014 |
wenzelm <none@none> |
proper context;
|
#
4de86cb2 |
|
09-Nov-2014 |
wenzelm <none@none> |
proper context for match_tac etc.;
|
#
d6623f99 |
|
09-Nov-2014 |
wenzelm <none@none> |
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
|
#
16b4f761 |
|
08-Nov-2014 |
wenzelm <none@none> |
optional proof context for unify operations, for the sake of proper local options;
|
#
2d556eb3 |
|
30-Oct-2014 |
wenzelm <none@none> |
eliminated aliases;
|
#
f9cb1a7a |
|
29-Oct-2014 |
wenzelm <none@none> |
modernized setup;
|
#
69aa9816 |
|
04-Jul-2014 |
wenzelm <none@none> |
more uniform names;
|
#
9fd71573 |
|
10-Jun-2014 |
Thomas Sewell <thomas.sewell@nicta.com.au> |
Hypsubst preserves equality hypotheses Fixes included for various theories affected by this change. --HG-- extra : rebase_source : b0150e06a14c2821e03208834282be6eca87aae0
|
#
2c8d6176 |
|
21-Mar-2014 |
wenzelm <none@none> |
more qualified names;
|
#
e712bb09 |
|
24-May-2013 |
wenzelm <none@none> |
tuned signature;
|
#
0e2280bb |
|
27-Apr-2013 |
wenzelm <none@none> |
uniform Proof.context for hyp_subst_tac;
|
#
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
#
eacead9b |
|
08-Nov-2012 |
bulwahn <none@none> |
hyp_subst_tac allows to pass an optional simpset to the internal simplifier call to avoid renamed bound variable warnings in the simplifier call
|
#
4c6bd77d |
|
19-Jun-2012 |
Rafal Kolanski <rafal.kolanski@nicta.com.au> |
Updated comment to reflect current state. --HG-- extra : rebase_source : cca9fff2cbe5f8deae7a5d9b6aaf251a035993ed
|
#
cfb69d7d |
|
14-Jan-2012 |
wenzelm <none@none> |
discontinued old-style Term.list_abs in favour of plain Term.abs;
|
#
f21371f9 |
|
28-Nov-2011 |
wenzelm <none@none> |
avoid stepping outside of context -- plain zero_var_indexes should be sufficient;
|
#
1d553e50 |
|
24-Nov-2011 |
wenzelm <none@none> |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
#
4911f028 |
|
08-Aug-2011 |
wenzelm <none@none> |
misc tuning -- eliminated old-fashioned rep_thm;
|
#
d599c840 |
|
09-Jun-2011 |
wenzelm <none@none> |
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
|
#
a6a9e8cb |
|
14-May-2011 |
wenzelm <none@none> |
modernized functor names; tuned;
|
#
326d17da |
|
16-Apr-2011 |
wenzelm <none@none> |
more direct Thm.cprem_of (with exception THM instead of Subscript);
|
#
d1a2ff7b |
|
16-Apr-2011 |
wenzelm <none@none> |
eliminated old List.nth; tuned;
|
#
fea60320 |
|
24-Mar-2011 |
wenzelm <none@none> |
more direct loose_bvar1; tuned;
|
#
d74c032d |
|
29-Sep-2010 |
krauss <none@none> |
backed out my old attempt at single_hyp_subst_tac (67cd6ed76446) It never was totally reliable, and better alternatives now exist (Subgoal.FOCUS).
|
#
8567a5f5 |
|
10-Sep-2010 |
krauss <none@none> |
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
|
#
dc514061 |
|
15-May-2010 |
wenzelm <none@none> |
less pervasive names from structure Thm;
|
#
b96c5111 |
|
29-Apr-2010 |
wenzelm <none@none> |
proper context for mksimps etc. -- via simpset of the running Simplifier;
|
#
458a4961 |
|
13-Mar-2010 |
wenzelm <none@none> |
removed old CVS Ids; tuned headers;
|
#
aa047a26 |
|
19-Feb-2010 |
wenzelm <none@none> |
renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
|
#
2396d686 |
|
07-Feb-2010 |
wenzelm <none@none> |
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
|
#
a2aef54e |
|
16-Oct-2009 |
wenzelm <none@none> |
explicitly qualify Drule.standard;
|
#
be04b5a8 |
|
13-Mar-2009 |
wenzelm <none@none> |
simplified method setup;
|
#
77d6b267 |
|
13-Mar-2009 |
wenzelm <none@none> |
unified type Proof.method and pervasive METHOD combinators;
|
#
c158a8c2 |
|
04-Aug-2008 |
wenzelm <none@none> |
meta_subst: xsymbols make it work with clean Pure;
|
#
c34acdea |
|
14-Jul-2008 |
krauss <none@none> |
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
|
#
619e3311 |
|
24-May-2008 |
wenzelm <none@none> |
inst_subst_tac: match types -- no longer assume that subst rule has exactly one type argument; misc tuning -- more cterm operations, more qualified names;
|
#
b8a5349a |
|
07-May-2008 |
berghofe <none@none> |
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.
|
#
219b0e06 |
|
22-Jul-2007 |
wenzelm <none@none> |
blast_hyp_subst_tac: plain bool argument;
|
#
f7800759 |
|
29-Nov-2006 |
wenzelm <none@none> |
simplified method setup;
|
#
31ac18a7 |
|
07-Nov-2006 |
wenzelm <none@none> |
avoid handling of arbitrary exceptions;
|
#
d18b4bc2 |
|
07-Nov-2006 |
wenzelm <none@none> |
simplified dest_eq; do not export debuging stuff; has_tvars: actually check all types within a term, not just its resulting type; tuned;
|
#
65eebeb7 |
|
11-Oct-2006 |
haftmann <none@none> |
slight type signature changes
|
#
43e22170 |
|
10-Oct-2006 |
haftmann <none@none> |
fixed intendation
|
#
4f3c0a34 |
|
10-Jul-2006 |
wenzelm <none@none> |
Name.is_bound;
|
#
75fddbe8 |
|
19-Jan-2006 |
wenzelm <none@none> |
setup: theory -> theory;
|
#
25501e62 |
|
18-Oct-2005 |
wenzelm <none@none> |
functor: no Simplifier argument; Simplifier.theory_context;
|
#
bd7d8e3c |
|
01-Aug-2005 |
wenzelm <none@none> |
Term.is_bound;
|
#
3275b5bb |
|
07-Apr-2005 |
wenzelm <none@none> |
improved comments;
|
#
3dffd254 |
|
13-Feb-2005 |
skalberg <none@none> |
Deleted Library.option type.
|
#
883f343f |
|
01-Feb-2005 |
paulson <none@none> |
the new subst tactic, by Lucas Dixon
|
#
c65b4145 |
|
15-Dec-2004 |
paulson <none@none> |
fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions
|
#
9942e5df |
|
30-Sep-2002 |
berghofe <none@none> |
- 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
|
#
df70136b |
|
04-Dec-2001 |
wenzelm <none@none> |
'symmetric' attribute moved to Pure/calculation.ML;
|
#
4e645f36 |
|
20-Nov-2001 |
wenzelm <none@none> |
use tracing function for trace output;
|
#
07b92609 |
|
07-Jan-2001 |
wenzelm <none@none> |
CHANGED_PROP;
|
#
725596cb |
|
07-Sep-2000 |
wenzelm <none@none> |
tuned msg;
|
#
67166d02 |
|
28-Aug-2000 |
wenzelm <none@none> |
Method.SIMPLE_METHOD';
|
#
524bc1c6 |
|
17-Aug-2000 |
wenzelm <none@none> |
added 'symmetric' attribute;
|
#
3be28a66 |
|
14-Aug-2000 |
wenzelm <none@none> |
added hypsubst;
|
#
80ac2a67 |
|
04-Aug-2000 |
wenzelm <none@none> |
added rev_eq_reflection; export stac; proof method setup: subst, hypsubst;
|
#
bf0f5424 |
|
23-Dec-1997 |
paulson <none@none> |
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
|
#
fb7ff37c |
|
26-Nov-1997 |
paulson <none@none> |
updated comment
|
#
5310779e |
|
12-Nov-1997 |
oheimb <none@none> |
added thin_refl to hyp_subst_tac
|
#
8b7e75b4 |
|
06-Nov-1997 |
paulson <none@none> |
hyp_subst_tac checks if the equality has type variables and uses a suitable method if so. Affects the dest_eq function
|
#
f21d92b1 |
|
22-Jul-1997 |
paulson <none@none> |
Removal of the tactical STATE
|
#
e3990973 |
|
07-Mar-1997 |
paulson <none@none> |
Prevent permutation of assumptions in hyp_subst_tac
|
#
8eaeaed6 |
|
05-Mar-1997 |
paulson <none@none> |
Now uses rotate_tac and eta_contract_atom for greater speed
|
#
3227d1e3 |
|
12-Nov-1996 |
paulson <none@none> |
Removed a call to polymorphic mem
|
#
b5ed428c |
|
01-Nov-1996 |
paulson <none@none> |
Replaced min by Int.min
|
#
4fbb8504 |
|
06-Apr-1995 |
lcp <none@none> |
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.
|
#
625f0a2b |
|
11-Nov-1994 |
lcp <none@none> |
Provers/hypsubst/REPEATN: deleted; using REPEAT_DETERM_N instead.
|
#
34e1169a |
|
01-Nov-1994 |
lcp <none@none> |
Provers/hypsubst: greatly simplified! No longer simulates a "eres_inst_tac" using rev_cut_eq; instead simply rotates the chosen equality to the end!
|
#
cefc6ce4 |
|
19-Oct-1994 |
lcp <none@none> |
new comments explaining abandoned change
|
#
88a6e5a8 |
|
18-Jan-1994 |
lcp <none@none> |
Updated refs to old Sign functions
|
#
f253ef6a |
|
15-Sep-1993 |
clasohm <none@none> |
Initial revision
|