| Sat, 27 Feb 2010 23:13:01 +0100 |
wenzelm |
modernized structure Term_Ord;
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 20:41:34 +0100 |
wenzelm |
Thm.def_binding;
|
file |
diff |
annotate
|
| Mon, 16 Nov 2009 13:53:31 +0100 |
wenzelm |
eliminated obsolete thm position stuff;
|
file |
diff |
annotate
|
| Sun, 15 Nov 2009 15:14:28 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 17:25:09 +0100 |
wenzelm |
eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 22:29:54 +0100 |
wenzelm |
eliminated slightly odd (unused) "axiom" and "assumption" -- collapsed to unspecific "";
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 22:02:11 +0100 |
wenzelm |
eliminated obsolete "internal" kind -- collapsed to unspecific "";
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 20:40:16 +0100 |
wenzelm |
scalable version of Named_Thms, using Item_Net;
|
file |
diff |
annotate
|
| Sun, 01 Nov 2009 20:59:34 +0100 |
wenzelm |
adapted Item_Net;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 16:34:44 +0100 |
wenzelm |
eliminated obsolete/unused Thm.kind_internal/is_internal etc.;
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 19:18:59 +0100 |
wenzelm |
maintain group via name space, not tags;
|
file |
diff |
annotate
|
| Thu, 01 Oct 2009 22:40:29 +0200 |
wenzelm |
added Ctermtab, cterm_cache, thm_cache;
|
file |
diff |
annotate
|
| Thu, 30 Jul 2009 01:12:33 +0200 |
wenzelm |
added certify_inst, certify_instantiate;
|
file |
diff |
annotate
|
| Sun, 26 Jul 2009 13:12:53 +0200 |
wenzelm |
lambda/cabs/all: named variants;
|
file |
diff |
annotate
|
| Thu, 09 Jul 2009 22:48:12 +0200 |
wenzelm |
renamed structure TermSubst to Term_Subst;
|
file |
diff |
annotate
|
| Thu, 09 Jul 2009 22:01:41 +0200 |
wenzelm |
renamed functor TableFun to Table, and GraphFun to Graph;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2009 22:42:27 +0200 |
wenzelm |
clarified strip_shyps: proper type witnesses for present sorts;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2009 20:36:38 +0200 |
wenzelm |
clarified Thm.of_class/of_sort/class_triv;
|
file |
diff |
annotate
|
| Thu, 02 Jul 2009 21:26:18 +0200 |
wenzelm |
renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);
|
file |
diff |
annotate
|
| Mon, 18 May 2009 09:48:06 +0200 |
haftmann |
introduced Thm.generatedK
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Tue, 17 Mar 2009 15:34:42 +0100 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
| Tue, 17 Mar 2009 14:12:43 +0100 |
wenzelm |
adapted to general Item_Net;
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 15:36:12 +0100 |
wenzelm |
added def_binding_optional -- robust version of def_name_optional for bindings;
|
file |
diff |
annotate
|
| Sat, 07 Mar 2009 22:04:59 +0100 |
wenzelm |
moved Thm.def_name(_optional) to more_thm.ML;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2009 14:07:23 +0100 |
wenzelm |
added type binding and val empty_binding;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:04 +0100 |
haftmann |
binding replaces bstring
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 15:30:10 +0100 |
wenzelm |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
| Thu, 23 Oct 2008 15:28:01 +0200 |
wenzelm |
renamed Thm.get_axiom_i to Thm.axiom;
|
file |
diff |
annotate
|
| Thu, 16 Oct 2008 22:44:30 +0200 |
wenzelm |
added check_shyps, which reject pending sort hypotheses;
|
file |
diff |
annotate
|
| Wed, 03 Sep 2008 17:50:37 +0200 |
wenzelm |
simplified add_axiom: no hyps;
|
file |
diff |
annotate
|
| Wed, 27 Aug 2008 11:48:54 +0200 |
wenzelm |
type Properties.T;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2008 16:52:51 +0200 |
wenzelm |
moved basic thm operations from structure PureThy to Thm;
|
file |
diff |
annotate
|
| Wed, 18 Jun 2008 18:55:03 +0200 |
wenzelm |
removed obsolete read_def_cterms/read_cterm;
|
file |
diff |
annotate
|
| Tue, 15 Apr 2008 18:49:19 +0200 |
wenzelm |
Theory.eq_thy;
|
file |
diff |
annotate
|
| Tue, 15 Apr 2008 16:12:05 +0200 |
wenzelm |
Thm.forall_elim_var(s);
|
file |
diff |
annotate
|
| Sat, 12 Apr 2008 17:00:40 +0200 |
wenzelm |
replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
|
file |
diff |
annotate
|
| Mon, 03 Dec 2007 16:04:16 +0100 |
haftmann |
interface for unchecked definitions
|
file |
diff |
annotate
|
| Thu, 11 Oct 2007 19:10:22 +0200 |
wenzelm |
added elim_implies (more convenient argument order);
|
file |
diff |
annotate
|
| Wed, 10 Oct 2007 17:31:55 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 30 Sep 2007 16:20:37 +0200 |
wenzelm |
Markup.internalK;
|
file |
diff |
annotate
|
| Sun, 29 Jul 2007 14:30:04 +0200 |
wenzelm |
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
|
file |
diff |
annotate
|
| Thu, 05 Jul 2007 20:01:36 +0200 |
wenzelm |
added is_reflexive;
|
file |
diff |
annotate
|
| Mon, 25 Jun 2007 00:36:40 +0200 |
wenzelm |
added reasonably efficient add_cterm_frees;
|
file |
diff |
annotate
|
| Thu, 31 May 2007 19:11:19 +0200 |
wenzelm |
made aconvc pervasive;
|
file |
diff |
annotate
|
| Thu, 31 May 2007 18:31:36 +0200 |
wenzelm |
moved aconvc to more_thm.ML;
|
file |
diff |
annotate
|
| Thu, 10 May 2007 00:39:53 +0200 |
wenzelm |
added destructors from drule.ML;
|
file |
diff |
annotate
|
| Sun, 15 Apr 2007 14:31:53 +0200 |
wenzelm |
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
|
file |
diff |
annotate
|
| Sat, 14 Apr 2007 17:36:10 +0200 |
wenzelm |
added read_def_cterms, read_cterm (from thm.ML);
|
file |
diff |
annotate
|
| Wed, 28 Feb 2007 22:05:43 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 26 Feb 2007 23:18:27 +0100 |
wenzelm |
Further operations on type thm, outside the inference kernel.
|
file |
diff |
annotate
|