src/Pure/drule.ML
Wed, 29 May 2013 18:25:11 +0200 wenzelm tuned signature -- more explicit flags for low-level Thm.bicompose;
Fri, 24 May 2013 17:00:46 +0200 wenzelm tuned signature;
Mon, 25 Jun 2012 17:50:05 +0200 wenzelm eliminated obsolete swap_prems_rl -- rotate_prems usually does the job more directly;
Wed, 11 Apr 2012 21:40:46 +0200 wenzelm rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
Sat, 31 Mar 2012 19:26:23 +0200 wenzelm tuned signature;
Mon, 19 Mar 2012 21:10:33 +0100 wenzelm moved some legacy stuff;
Wed, 15 Feb 2012 23:19:30 +0100 wenzelm renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
Wed, 15 Feb 2012 22:44:31 +0100 wenzelm discontinued Drule.term_rule, which tends to cause confusion due to builtin cterm_of (NB: the standard morphisms already provide a separate term component);
Tue, 14 Feb 2012 20:57:05 +0100 wenzelm discontinued unused MRL -- in correspondence with section "2.4.2 Rule composition" in the implementation manual;
Sat, 14 Jan 2012 16:58:29 +0100 wenzelm tuned;
Wed, 11 Jan 2012 16:25:34 +0100 wenzelm more qualified names;
Sat, 05 Nov 2011 20:32:12 +0100 wenzelm tuned cterm_instantiate: avoid somewhat expensive Term.map_types and cterm_of;
Sat, 05 Nov 2011 20:07:38 +0100 wenzelm misc tuning and modernization;
Sun, 16 Oct 2011 18:48:30 +0200 wenzelm added Term.dummy_pattern conveniences;
Wed, 10 Aug 2011 19:45:41 +0200 wenzelm avoid OldTerm operations -- with subtle changes of semantics;
Mon, 27 Jun 2011 15:03:55 +0200 wenzelm old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;
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;
Thu, 09 Jun 2011 20:56:08 +0200 wenzelm clarified special incr_type_indexes;
Thu, 09 Jun 2011 16:34:49 +0200 wenzelm discontinued Name.variant to emphasize that this is old-style / indirect;
Sat, 23 Apr 2011 19:41:53 +0200 wenzelm hardwired mapping "_" -> "Pure.asm_rl" avoids legacy binding;
Fri, 26 Nov 2010 22:29:41 +0100 wenzelm make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
Mon, 20 Sep 2010 16:05:25 +0200 wenzelm renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
Wed, 25 Aug 2010 15:12:49 +0200 wenzelm structure Thm: less pervasive names;
Sat, 15 May 2010 21:41:32 +0200 wenzelm less pervasive names from structure Thm;
Mon, 03 May 2010 20:13:36 +0200 wenzelm renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
Sun, 25 Apr 2010 23:09:32 +0200 wenzelm renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp;
Sat, 27 Mar 2010 15:20:31 +0100 wenzelm moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
Mon, 22 Mar 2010 19:29:11 +0100 wenzelm eliminated old-style Drule.add_axiom in favour of Specification.axiom, with explicit Drule.export_without_context to imitate the old behaviour;
Mon, 22 Mar 2010 00:48:56 +0100 wenzelm replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;
Sat, 20 Mar 2010 17:33:11 +0100 wenzelm renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
Fri, 19 Feb 2010 20:39:48 +0100 wenzelm moved ancient Drule.get_def to OldGoals.get_def;
Sun, 07 Feb 2010 19:33:34 +0100 wenzelm renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
Sat, 21 Nov 2009 15:49:29 +0100 wenzelm explicitly mark some legacy freeze operations;
Thu, 12 Nov 2009 22:02:11 +0100 wenzelm eliminated obsolete "internal" kind -- collapsed to unspecific "";
Mon, 02 Nov 2009 20:34:59 +0100 wenzelm modernized structure Simple_Syntax;
Wed, 28 Oct 2009 16:25:26 +0100 wenzelm Drule.store: proper binding;
Sat, 24 Oct 2009 19:47:37 +0200 wenzelm renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
Sat, 17 Oct 2009 00:53:18 +0200 wenzelm legacy Drule.standard is no longer pervasive;
Thu, 09 Jul 2009 22:48:12 +0200 wenzelm renamed structure TermSubst to Term_Subst;
Mon, 06 Jul 2009 21:24:30 +0200 wenzelm structure Thm: less pervasive names;
Thu, 02 Jul 2009 21:26:18 +0200 wenzelm renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);
Mon, 16 Mar 2009 23:39:44 +0100 wenzelm refined is_norm_hhf: reject beta-redexes (rules based on term nets or could_unify assume normal form), also potentially faster by avoiding expensive Envir.beta_eta_contract;
Sat, 07 Mar 2009 22:04:59 +0100 wenzelm moved Thm.def_name(_optional) to more_thm.ML;
Wed, 21 Jan 2009 16:47:04 +0100 haftmann binding replaces bstring
Sun, 04 Jan 2009 15:28:09 +0100 wenzelm added comp_no_flatten;
Wed, 31 Dec 2008 18:53:16 +0100 wenzelm moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
Wed, 31 Dec 2008 00:08:13 +0100 wenzelm moved old add_term_vars, add_term_frees etc. to structure OldTerm;
Fri, 31 Oct 2008 10:39:04 +0100 berghofe Theorem "_" is now stored with open derivation.
Thu, 23 Oct 2008 15:28:01 +0200 wenzelm renamed Thm.get_axiom_i to Thm.axiom;
Thu, 16 Oct 2008 22:44:27 +0200 wenzelm added rules for sort_constraint, include in norm_hhf_eqs;
Thu, 14 Aug 2008 16:52:46 +0200 wenzelm moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
Mon, 23 Jun 2008 23:45:46 +0200 wenzelm Logic.implies;
Thu, 19 Jun 2008 20:48:03 +0200 wenzelm moved add_used to Isar/rule_insts.ML;
Mon, 16 Jun 2008 22:13:47 +0200 wenzelm removed obsolete global read_insts/read_instantiate (cf. Isar/rule_insts.ML);
Wed, 11 Jun 2008 18:03:14 +0200 wenzelm qualified types_sorts, read_insts etc.;
Sun, 18 May 2008 15:04:09 +0200 wenzelm moved global pretty/string_of functions from Sign to Syntax;
Tue, 15 Apr 2008 16:12:05 +0200 wenzelm Thm.forall_elim_var(s);
Sat, 12 Apr 2008 17:00:38 +0200 wenzelm rep_cterm/rep_thm: no longer dereference theory_ref;
Sat, 29 Mar 2008 19:14:09 +0100 wenzelm certify wrt. dynamic context;
Thu, 27 Mar 2008 14:41:09 +0100 wenzelm eliminated theory ProtoPure;
less more (0) -300 -100 -60 tip