| Thu, 03 Feb 2011 20:13:49 +0100 |
wenzelm |
thm_proof: visible fulfill_body only, without joining nested thms -- retain proof irrelevance, which is important for parallel performance;
|
file |
diff |
annotate
|
| Thu, 03 Feb 2011 19:27:04 +0100 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| 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
|