| Thu, 28 Oct 2010 22:23:11 +0200 |
wenzelm |
type attribute is derived concept outside the kernel;
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 11:22:30 +0200 |
wenzelm |
recovered some odd two-dimensional layout;
|
file |
diff |
annotate
|
| Fri, 24 Sep 2010 15:53:13 +0200 |
wenzelm |
modernized structure Ord_List;
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 15:12:49 +0200 |
wenzelm |
structure Thm: less pervasive names;
|
file |
diff |
annotate
|
| Thu, 03 Jun 2010 23:17:57 +0200 |
wenzelm |
eliminated ML structure alias;
|
file |
diff |
annotate
|
| Wed, 02 Jun 2010 21:39:35 +0200 |
wenzelm |
always unconstrain thm proofs;
|
file |
diff |
annotate
|
| Wed, 19 May 2010 10:17:05 +0200 |
haftmann |
dropped legacy_unconstrainT
|
file |
diff |
annotate
|
| Fri, 14 May 2010 19:53:36 +0200 |
wenzelm |
added Proofterm.unconstrain_thm_proof for Thm.unconstrainT -- loosely based on the version by krauss/schropp;
|
file |
diff |
annotate
|
| Thu, 13 May 2010 21:36:38 +0200 |
wenzelm |
conditionally unconstrain thm proofs -- loosely based on the version by krauss/schropp;
|
file |
diff |
annotate
|
| Sun, 09 May 2010 22:06:24 +0200 |
wenzelm |
reactivated Thm.legacy_unconstrainT for Nbe.lift_triv_classes_conv;
|
file |
diff |
annotate
|
| Sun, 09 May 2010 19:50:56 +0200 |
wenzelm |
Thm.unconstrainT based on Logic.unconstrainT -- no proofterm yet;
|
file |
diff |
annotate
|
| Sun, 09 May 2010 19:15:21 +0200 |
wenzelm |
just one version of Thm.unconstrainT, which affects all variables;
|
file |
diff |
annotate
|
| 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
|
| Sat, 08 May 2010 16:24:44 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 04 May 2010 14:38:59 +0200 |
wenzelm |
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
|
file |
diff |
annotate
|
| Tue, 04 May 2010 11:02:50 +0200 |
wenzelm |
renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);
|
file |
diff |
annotate
|
| Mon, 03 May 2010 20:13:36 +0200 |
wenzelm |
renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
|
file |
diff |
annotate
|
| Mon, 03 May 2010 16:26:47 +0200 |
wenzelm |
minor tuning of Thm.strip_shyps -- no longer pervasive;
|
file |
diff |
annotate
|
| Mon, 03 May 2010 15:34:55 +0200 |
wenzelm |
simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here;
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 23:09:32 +0200 |
wenzelm |
renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp;
|
file |
diff |
annotate
|
| Sat, 27 Mar 2010 15:47:57 +0100 |
wenzelm |
added Term.fold_atyps_sorts convenience;
|
file |
diff |
annotate
|
| Sun, 21 Mar 2010 22:13:31 +0100 |
wenzelm |
Logic.mk_of_sort convenience;
|
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
|
| Sat, 27 Feb 2010 23:13:01 +0100 |
wenzelm |
modernized structure Term_Ord;
|
file |
diff |
annotate
|
| Wed, 25 Nov 2009 09:13:46 +0100 |
haftmann |
normalized uncurry take/drop
|
file |
diff |
annotate
|
| Tue, 24 Nov 2009 17:28:25 +0100 |
haftmann |
curried take/drop
|
file |
diff |
annotate
|
| Sat, 21 Nov 2009 15:49:29 +0100 |
wenzelm |
explicitly mark some legacy freeze operations;
|
file |
diff |
annotate
|
| Mon, 16 Nov 2009 21:57:16 +0100 |
wenzelm |
generalized procs for rewrite_proof: allow skeleton;
|
file |
diff |
annotate
|
| Sun, 15 Nov 2009 15:14:28 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 18:43:42 +0100 |
wenzelm |
adapted Theory_Data;
|
file |
diff |
annotate
|