src/Pure/more_thm.ML
Thu, 28 Oct 2010 22:23:11 +0200 wenzelm type attribute is derived concept outside the kernel;
Sun, 05 Sep 2010 19:47:40 +0200 wenzelm pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
Sat, 08 May 2010 16:53:53 +0200 wenzelm renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;
Sun, 11 Apr 2010 14:30:34 +0200 wenzelm Thm.add_axiom/add_def: return internal name of foundational axiom;
Sat, 27 Mar 2010 17:36:32 +0100 wenzelm disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
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 00:51:18 +0100 wenzelm replaced Theory.add_axioms(_i) by more primitive Theory.add_axiom;
Sun, 21 Mar 2010 22:24:04 +0100 wenzelm add_axiom: axiomatize "unconstrained" version, with explicit of_class premises;
Sun, 21 Mar 2010 19:30:19 +0100 wenzelm more explicit invented name;
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;
Thu, 11 Mar 2010 23:07:02 +0100 wenzelm tuned;
Sat, 27 Feb 2010 23:13:01 +0100 wenzelm modernized structure Term_Ord;
Fri, 19 Feb 2010 20:41:34 +0100 wenzelm Thm.def_binding;
Mon, 16 Nov 2009 13:53:31 +0100 wenzelm eliminated obsolete thm position stuff;
Sun, 15 Nov 2009 15:14:28 +0100 wenzelm tuned;
Fri, 13 Nov 2009 17:25:09 +0100 wenzelm eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);
Thu, 12 Nov 2009 22:29:54 +0100 wenzelm eliminated slightly odd (unused) "axiom" and "assumption" -- collapsed to unspecific "";
Thu, 12 Nov 2009 22:02:11 +0100 wenzelm eliminated obsolete "internal" kind -- collapsed to unspecific "";
Thu, 05 Nov 2009 20:40:16 +0100 wenzelm scalable version of Named_Thms, using Item_Net;
Sun, 01 Nov 2009 20:59:34 +0100 wenzelm adapted Item_Net;
Thu, 29 Oct 2009 16:34:44 +0100 wenzelm eliminated obsolete/unused Thm.kind_internal/is_internal etc.;
Sun, 25 Oct 2009 19:18:59 +0100 wenzelm maintain group via name space, not tags;
Thu, 01 Oct 2009 22:40:29 +0200 wenzelm added Ctermtab, cterm_cache, thm_cache;
Thu, 30 Jul 2009 01:12:33 +0200 wenzelm added certify_inst, certify_instantiate;
Sun, 26 Jul 2009 13:12:53 +0200 wenzelm lambda/cabs/all: named variants;
Thu, 09 Jul 2009 22:48:12 +0200 wenzelm renamed structure TermSubst to Term_Subst;
Thu, 09 Jul 2009 22:01:41 +0200 wenzelm renamed functor TableFun to Table, and GraphFun to Graph;
Mon, 06 Jul 2009 22:42:27 +0200 wenzelm clarified strip_shyps: proper type witnesses for present sorts;
Mon, 06 Jul 2009 20:36:38 +0200 wenzelm clarified Thm.of_class/of_sort/class_triv;
Thu, 02 Jul 2009 21:26:18 +0200 wenzelm renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);
Mon, 18 May 2009 09:48:06 +0200 haftmann introduced Thm.generatedK
Sat, 16 May 2009 20:17:59 +0200 bulwahn added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages
Tue, 17 Mar 2009 15:34:42 +0100 wenzelm tuned comment;
Tue, 17 Mar 2009 14:12:43 +0100 wenzelm adapted to general Item_Net;
Wed, 11 Mar 2009 15:36:12 +0100 wenzelm added def_binding_optional -- robust version of def_name_optional for bindings;
Sat, 07 Mar 2009 22:04:59 +0100 wenzelm moved Thm.def_name(_optional) to more_thm.ML;
Tue, 03 Mar 2009 14:07:23 +0100 wenzelm added type binding and val empty_binding;
Wed, 21 Jan 2009 16:47:04 +0100 haftmann binding replaces bstring
Wed, 31 Dec 2008 15:30:10 +0100 wenzelm moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
Thu, 04 Dec 2008 14:43:33 +0100 haftmann cleaned up binding module and related code
Thu, 23 Oct 2008 15:28:01 +0200 wenzelm renamed Thm.get_axiom_i to Thm.axiom;
Thu, 16 Oct 2008 22:44:30 +0200 wenzelm added check_shyps, which reject pending sort hypotheses;
Wed, 03 Sep 2008 17:50:37 +0200 wenzelm simplified add_axiom: no hyps;
Wed, 27 Aug 2008 11:48:54 +0200 wenzelm type Properties.T;
Thu, 14 Aug 2008 16:52:51 +0200 wenzelm moved basic thm operations from structure PureThy to Thm;
Wed, 18 Jun 2008 18:55:03 +0200 wenzelm removed obsolete read_def_cterms/read_cterm;
Tue, 15 Apr 2008 18:49:19 +0200 wenzelm Theory.eq_thy;
Tue, 15 Apr 2008 16:12:05 +0200 wenzelm Thm.forall_elim_var(s);
Sat, 12 Apr 2008 17:00:40 +0200 wenzelm replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
Mon, 03 Dec 2007 16:04:16 +0100 haftmann interface for unchecked definitions
Thu, 11 Oct 2007 19:10:22 +0200 wenzelm added elim_implies (more convenient argument order);
Wed, 10 Oct 2007 17:31:55 +0200 wenzelm tuned;
Sun, 30 Sep 2007 16:20:37 +0200 wenzelm Markup.internalK;
Sun, 29 Jul 2007 14:30:04 +0200 wenzelm moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
Thu, 05 Jul 2007 20:01:36 +0200 wenzelm added is_reflexive;
Mon, 25 Jun 2007 00:36:40 +0200 wenzelm added reasonably efficient add_cterm_frees;
Thu, 31 May 2007 19:11:19 +0200 wenzelm made aconvc pervasive;
Thu, 31 May 2007 18:31:36 +0200 wenzelm moved aconvc to more_thm.ML;
Thu, 10 May 2007 00:39:53 +0200 wenzelm added destructors from drule.ML;
Sun, 15 Apr 2007 14:31:53 +0200 wenzelm moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
less more (0) -60 tip