| #
1e698ab2 |
|
25-Feb-2018 |
wenzelm <none@none> |
eliminated ASCII syntax from Pure bootstrap;
tuned comments;
|
| #
5f318eee |
|
04-Mar-2015 |
wenzelm <none@none> |
clarified signature;
|
| #
2c8d6176 |
|
21-Mar-2014 |
wenzelm <none@none> |
more qualified names;
|
| #
9a62c4aa |
|
30-Dec-2012 |
wenzelm <none@none> |
tuned -- recovered comments from 791157a4179a;
|
| #
8e5721df |
|
24-Oct-2012 |
nipkow <none@none> |
ensured that rewr_conv rule t = "t == u" literally not just modulo beta-eta
|
| #
d599c840 |
|
09-Jun-2011 |
wenzelm <none@none> |
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
|
| #
12d6e22f |
|
27-Apr-2011 |
wenzelm <none@none> |
tuned;
|
| #
aa091a5d |
|
17-Dec-2010 |
haftmann <none@none> |
dropped slightly odd Conv.tap_thy
|
| #
fa0dfbef |
|
23-Aug-2010 |
haftmann <none@none> |
tap_thy conversional
|
| #
4d41603e |
|
15-May-2010 |
wenzelm <none@none> |
incorporated further conversions and conversionals, after some minor tuning;
|
| #
79dfcda4 |
|
01-Oct-2009 |
wenzelm <none@none> |
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
|
| #
121e82fb |
|
04-Mar-2009 |
blanchet <none@none> |
Merge.
|
| #
b52bec42 |
|
26-Feb-2009 |
boehmes <none@none> |
Made then_conv and else_conv available as infix operations.
|
| #
1bd59ac7 |
|
21-Jan-2009 |
wenzelm <none@none> |
removed Ids;
|
| #
e6984cd2 |
|
23-Jun-2008 |
wenzelm <none@none> |
Logic.is_all;
|
| #
532f8f27 |
|
07-Apr-2008 |
wenzelm <none@none> |
abs_conv: extra argument for bound variable;
renamed iterated forall_conv to params_conv;
added forall_conv, implies_conv, implies_concl_conv, rewr_conv;
|
| #
90811e91 |
|
25-Feb-2008 |
wenzelm <none@none> |
tuned;
|
| #
bee29a76 |
|
04-Oct-2007 |
wenzelm <none@none> |
abs_conv/forall_conv: proper context (avoid gensym);
removed unused cache_conv;
|
| #
209b8a63 |
|
08-Jul-2007 |
wenzelm <none@none> |
gensym: slightly more obscure prefix descreases probability of name clash;
|
| #
84f3b70e |
|
05-Jul-2007 |
wenzelm <none@none> |
moved type conv to thm.ML;
renamed Conv.is_refl to Thm.is_reflexive;
misc tuning of basic conversions;
|
| #
6e05748a |
|
04-Jul-2007 |
wenzelm <none@none> |
tuned;
|
| #
d15db7b6 |
|
04-Jul-2007 |
wenzelm <none@none> |
else_conv: only handle THM | CTERM | TERM | TYPE;
prems_conv: no index;
renamed goal_conv_rule to gconv_rule;
|
| #
915297f3 |
|
03-Jul-2007 |
wenzelm <none@none> |
removed obsolete goals_conv (cf. prems_conv);
added efficient goal_conv_rule;
tuned comments;
|
| #
72be59c6 |
|
24-Jun-2007 |
wenzelm <none@none> |
made type conv pervasive;
removed obsolete eta_conv (cf. Thm.eta_long_conv);
|
| #
896391fa |
|
17-Jun-2007 |
chaieb <none@none> |
Added eta_conv and eta-expansion conversion: waiting for it to be in thm.ML; exported is_refl
|
| #
1a80356f |
|
31-May-2007 |
wenzelm <none@none> |
moved aconvc to more_thm.ML;
|
| #
7b39ae0f |
|
19-May-2007 |
chaieb <none@none> |
added binop_conv, aconvc
|
| #
5f945431 |
|
11-May-2007 |
wenzelm <none@none> |
unified names: foo_conv;
|
| #
b55ae304 |
|
10-May-2007 |
wenzelm <none@none> |
more conversions;
tuned;
|
| #
dd5404fb |
|
09-May-2007 |
wenzelm <none@none> |
Conversions: primitive equality reasoning (from drule.ML);
|