Mon, 18 Apr 2011 14:05:39 +0200 |
wenzelm |
pass plain Proof.context for pretty printing;
|
file |
diff |
annotate
|
Mon, 18 Apr 2011 11:44:39 +0200 |
wenzelm |
pass plain Proof.context for pretty printing;
|
file |
diff |
annotate
|
Mon, 18 Apr 2011 11:13:29 +0200 |
wenzelm |
simplified pretty printing context, which is only required for certain kernel operations;
|
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
|
Mon, 16 Nov 2009 13:53:02 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sun, 15 Nov 2009 20:39:22 +0100 |
wenzelm |
primitive defs: clarified def (axiom name) vs. description;
|
file |
diff |
annotate
|
Wed, 30 Sep 2009 22:24:57 +0200 |
wenzelm |
eliminated redundant parameters;
|
file |
diff |
annotate
|
Sat, 18 Jul 2009 00:34:22 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 17 Jul 2009 23:11:40 +0200 |
wenzelm |
tuned/modernized Envir.subst_XXX;
|
file |
diff |
annotate
|
Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
Mon, 01 Oct 2007 15:14:54 +0200 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
Thu, 09 Aug 2007 15:52:54 +0200 |
haftmann |
new access interface in defs.ML
|
file |
diff |
annotate
|
Thu, 21 Sep 2006 19:04:49 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Thu, 17 Aug 2006 09:24:48 +0200 |
haftmann |
renamed module to thyname
|
file |
diff |
annotate
|
Wed, 07 Jun 2006 02:01:28 +0200 |
wenzelm |
renamed Type.(un)varifyT to Logic.(un)varifyT;
|
file |
diff |
annotate
|
Fri, 02 Jun 2006 16:06:19 +0200 |
wenzelm |
merge: always normalize (and check!) reductions;
|
file |
diff |
annotate
|
Fri, 26 May 2006 22:20:03 +0200 |
wenzelm |
separate checks for acyclic/wellformed;
|
file |
diff |
annotate
|
Thu, 25 May 2006 16:51:39 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Wed, 24 May 2006 22:04:06 +0200 |
wenzelm |
made smlnj happy;
|
file |
diff |
annotate
|
Wed, 24 May 2006 21:58:09 +0200 |
wenzelm |
wellformed: be less ambitious about structural containment;
|
file |
diff |
annotate
|
Wed, 24 May 2006 01:05:01 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Tue, 23 May 2006 13:55:01 +0200 |
wenzelm |
export plain_args;
|
file |
diff |
annotate
|
Mon, 22 May 2006 22:29:15 +0200 |
wenzelm |
specifications_of: lhs/rhs represented as typargs;
|
file |
diff |
annotate
|
Sat, 20 May 2006 23:45:37 +0200 |
wenzelm |
made smlnj happy;
|
file |
diff |
annotate
|
Sat, 20 May 2006 23:37:02 +0200 |
wenzelm |
yet another re-implementation:
|
file |
diff |
annotate
|
Sat, 13 May 2006 02:51:37 +0200 |
wenzelm |
actually reject malformed defs;
|
file |
diff |
annotate
|
Fri, 12 May 2006 18:11:09 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 12 May 2006 01:01:08 +0200 |
wenzelm |
improved propagate_deps;
|
file |
diff |
annotate
|
Thu, 11 May 2006 19:15:13 +0200 |
wenzelm |
allow dependencies of disjoint collections of instances;
|
file |
diff |
annotate
|
Mon, 08 May 2006 17:40:06 +0200 |
wenzelm |
simple substructure test for typargs (independent type constructors);
|
file |
diff |
annotate
|