#
a67185f6 |
|
02-Mar-2020 |
haftmann <none@none> |
infrastructure for extraction of equations x = t from premises beneath meta-all --HG-- extra : rebase_source : 8bcc91c27655c862caf8a5c7a310c2b0e1cf2064
|
#
c1869c88 |
|
24-Jul-2015 |
wenzelm <none@none> |
proper 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;
|
#
2d556eb3 |
|
30-Oct-2014 |
wenzelm <none@none> |
eliminated aliases;
|
#
8aa502e5 |
|
12-Jan-2014 |
wenzelm <none@none> |
tuned signature; clarified context;
|
#
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
#
7f6fd60f |
|
22-Apr-2011 |
wenzelm <none@none> |
simplified Data signature;
|
#
c6e0bbb6 |
|
22-Apr-2011 |
wenzelm <none@none> |
misc tuning and simplification;
|
#
ebf09630 |
|
22-Apr-2011 |
wenzelm <none@none> |
misc tuning;
|
#
25416a4b |
|
22-Apr-2011 |
wenzelm <none@none> |
do not open ML structures;
|
#
b95224b1 |
|
22-Apr-2011 |
wenzelm <none@none> |
proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61); tuned signature;
|
#
6d2612c8 |
|
16-Apr-2011 |
wenzelm <none@none> |
modernized structure Proof_Context;
|
#
5eb8efe1 |
|
16-Aug-2010 |
nipkow <none@none> |
now works for schematic terms as well, thanks to Alex for the `how-to'
|
#
48e5d592 |
|
16-Aug-2010 |
blanchet <none@none> |
typos in comment
|
#
60d6d298 |
|
03-May-2010 |
wenzelm <none@none> |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
#
458a4961 |
|
13-Mar-2010 |
wenzelm <none@none> |
removed old CVS Ids; tuned headers;
|
#
457c080b |
|
18-May-2009 |
nipkow <none@none> |
fine-tuned elimination of comprehensions involving x=t.
|
#
334b16f4 |
|
16-May-2009 |
nipkow <none@none> |
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}" by the new simproc defColl_regroup. More precisely, the simproc pulls an equation x=t (or t=x) out of a nest of conjunctions to the front where the simp rule singleton_conj_conv(2) converts to "if".
|
#
d18fb037 |
|
07-Jul-2006 |
wenzelm <none@none> |
Goal.prove: context;
|
#
8cceae71 |
|
21-Oct-2005 |
wenzelm <none@none> |
Goal.prove;
|
#
593d5827 |
|
02-Aug-2005 |
wenzelm <none@none> |
simprocs: Simplifier.inherit_bounds;
|
#
3dffd254 |
|
13-Feb-2005 |
skalberg <none@none> |
Deleted Library.option type.
|
#
69fd4979 |
|
08-Jul-2004 |
wenzelm <none@none> |
adapted type of simprocs;
|
#
0553df8d |
|
08-Aug-2002 |
wenzelm <none@none> |
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
|
#
f2a20659 |
|
17-Dec-2001 |
nipkow <none@none> |
now permutations of quantifiers are allowed as well.
|
#
d032b770 |
|
29-Mar-2001 |
nipkow <none@none> |
generalization of 1 point rules for ALL
|
#
3115ce1a |
|
23-Mar-2001 |
nipkow <none@none> |
added simproc for bounded quantifiers
|
#
c89f915e |
|
27-Oct-1999 |
nipkow <none@none> |
Fixed a bug in the EX simproc.
|
#
e87bb0b2 |
|
27-Nov-1997 |
nipkow <none@none> |
Quantifier elimination procs.
|