| 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;
|
file |
diff |
annotate
|
| Sun, 11 Apr 2010 14:30:34 +0200 |
wenzelm |
Thm.add_axiom/add_def: return internal name of foundational axiom;
|
file |
diff |
annotate
|
| Sat, 27 Mar 2010 17:36:32 +0100 |
wenzelm |
disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 00:51:18 +0100 |
wenzelm |
replaced Theory.add_axioms(_i) by more primitive Theory.add_axiom;
|
file |
diff |
annotate
|
| Sun, 21 Mar 2010 22:24:04 +0100 |
wenzelm |
add_axiom: axiomatize "unconstrained" version, with explicit of_class premises;
|
file |
diff |
annotate
|
| Sun, 21 Mar 2010 19:30:19 +0100 |
wenzelm |
more explicit invented name;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Thu, 11 Mar 2010 23:07:02 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 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
|