src/Pure/conv.ML
Thu, 09 Sep 2021 15:45:27 +0200 wenzelm clarified modules;
Sun, 25 Feb 2018 15:44:46 +0100 wenzelm eliminated ASCII syntax from Pure bootstrap;
Wed, 04 Mar 2015 22:05:01 +0100 wenzelm clarified signature;
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
Sun, 30 Dec 2012 16:59:11 +0100 wenzelm tuned -- recovered comments from 791157a4179a;
Wed, 24 Oct 2012 17:40:56 +0200 nipkow ensured that rewr_conv rule t = "t == u" literally not just modulo beta-eta
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;
Wed, 27 Apr 2011 14:11:37 +0200 wenzelm tuned;
Fri, 17 Dec 2010 18:32:40 +0100 haftmann dropped slightly odd Conv.tap_thy
Mon, 23 Aug 2010 11:09:48 +0200 haftmann tap_thy conversional
Sat, 15 May 2010 17:59:06 +0200 wenzelm incorporated further conversions and conversionals, after some minor tuning;
Thu, 01 Oct 2009 23:27:05 +0200 wenzelm moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
Thu, 26 Feb 2009 18:00:08 +0100 boehmes Made then_conv and else_conv available as infix operations.
Wed, 21 Jan 2009 23:21:44 +0100 wenzelm removed Ids;
Mon, 23 Jun 2008 23:45:45 +0200 wenzelm Logic.is_all;
Mon, 07 Apr 2008 21:25:22 +0200 wenzelm abs_conv: extra argument for bound variable;
Mon, 25 Feb 2008 16:31:18 +0100 wenzelm tuned;
Thu, 04 Oct 2007 16:59:30 +0200 wenzelm abs_conv/forall_conv: proper context (avoid gensym);
Sun, 08 Jul 2007 19:52:04 +0200 wenzelm gensym: slightly more obscure prefix descreases probability of name clash;
Thu, 05 Jul 2007 20:01:33 +0200 wenzelm moved type conv to thm.ML;
Thu, 05 Jul 2007 00:15:44 +0200 wenzelm tuned;
Thu, 05 Jul 2007 00:06:22 +0200 wenzelm else_conv: only handle THM | CTERM | TERM | TYPE;
Tue, 03 Jul 2007 17:17:09 +0200 wenzelm removed obsolete goals_conv (cf. prems_conv);
Mon, 25 Jun 2007 00:36:39 +0200 wenzelm made type conv pervasive;
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
Thu, 31 May 2007 18:31:36 +0200 wenzelm moved aconvc to more_thm.ML;
Sat, 19 May 2007 18:19:45 +0200 chaieb added binop_conv, aconvc
Fri, 11 May 2007 18:46:50 +0200 wenzelm unified names: foo_conv;
Thu, 10 May 2007 18:10:32 +0200 wenzelm more conversions;
Thu, 10 May 2007 00:39:51 +0200 wenzelm Conversions: primitive equality reasoning (from drule.ML);
less more (0) tip