| Sun, 25 Feb 2018 15:44:46 +0100 |
wenzelm |
eliminated ASCII syntax from Pure bootstrap;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 22:05:01 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Sun, 30 Dec 2012 16:59:11 +0100 |
wenzelm |
tuned -- recovered comments from 791157a4179a;
|
file |
diff |
annotate
|
| Wed, 24 Oct 2012 17:40:56 +0200 |
nipkow |
ensured that rewr_conv rule t = "t == u" literally not just modulo beta-eta
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 23:12:02 +0200 |
wenzelm |
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 14:11:37 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 18:32:40 +0100 |
haftmann |
dropped slightly odd Conv.tap_thy
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 11:09:48 +0200 |
haftmann |
tap_thy conversional
|
file |
diff |
annotate
|
| Sat, 15 May 2010 17:59:06 +0200 |
wenzelm |
incorporated further conversions and conversionals, after some minor tuning;
|
file |
diff |
annotate
|
| Thu, 01 Oct 2009 23:27:05 +0200 |
wenzelm |
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
|
file |
diff |
annotate
|
| Thu, 26 Feb 2009 18:00:08 +0100 |
boehmes |
Made then_conv and else_conv available as infix operations.
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Mon, 23 Jun 2008 23:45:45 +0200 |
wenzelm |
Logic.is_all;
|
file |
diff |
annotate
|
| Mon, 07 Apr 2008 21:25:22 +0200 |
wenzelm |
abs_conv: extra argument for bound variable;
|
file |
diff |
annotate
|
| Mon, 25 Feb 2008 16:31:18 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 16:59:30 +0200 |
wenzelm |
abs_conv/forall_conv: proper context (avoid gensym);
|
file |
diff |
annotate
|
| 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
|