| Sun, 08 Jul 2007 19:52:04 +0200 |
wenzelm |
gensym: slightly more obscure prefix descreases probability of name clash;
|
file |
diff |
annotate
|
| Thu, 05 Jul 2007 20:01:33 +0200 |
wenzelm |
moved type conv to thm.ML;
|
file |
diff |
annotate
|
| Thu, 05 Jul 2007 00:15:44 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 05 Jul 2007 00:06:22 +0200 |
wenzelm |
else_conv: only handle THM | CTERM | TERM | TYPE;
|
file |
diff |
annotate
|
| Tue, 03 Jul 2007 17:17:09 +0200 |
wenzelm |
removed obsolete goals_conv (cf. prems_conv);
|
file |
diff |
annotate
|
| Mon, 25 Jun 2007 00:36:39 +0200 |
wenzelm |
made type conv pervasive;
|
file |
diff |
annotate
|
| Sun, 17 Jun 2007 13:39:48 +0200 |
chaieb |
Added eta_conv and eta-expansion conversion: waiting for it to be in thm.ML; exported is_refl
|
file |
diff |
annotate
|
| Thu, 31 May 2007 18:31:36 +0200 |
wenzelm |
moved aconvc to more_thm.ML;
|
file |
diff |
annotate
|
| Sat, 19 May 2007 18:19:45 +0200 |
chaieb |
added binop_conv, aconvc
|
file |
diff |
annotate
|
| Fri, 11 May 2007 18:46:50 +0200 |
wenzelm |
unified names: foo_conv;
|
file |
diff |
annotate
|
| Thu, 10 May 2007 18:10:32 +0200 |
wenzelm |
more conversions;
|
file |
diff |
annotate
|
| Thu, 10 May 2007 00:39:51 +0200 |
wenzelm |
Conversions: primitive equality reasoning (from drule.ML);
|
file |
diff |
annotate
|