| Fri, 23 Aug 2013 20:35:50 +0200 |
wenzelm |
added Theory.setup convenience;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 15:09:25 +0200 |
wenzelm |
type theory is purely value-oriented;
|
file |
diff |
annotate
|
| Thu, 30 May 2013 12:35:40 +0200 |
wenzelm |
standardized aliases;
|
file |
diff |
annotate
|
| Wed, 10 Apr 2013 15:30:19 +0200 |
wenzelm |
more standard module name Axclass (according to file name);
|
file |
diff |
annotate
|
| Wed, 10 Apr 2013 13:10:38 +0200 |
wenzelm |
formal proof context for axclass proofs;
|
file |
diff |
annotate
|
| Tue, 08 Jan 2013 12:50:57 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 08 Jan 2013 12:39:39 +0100 |
wenzelm |
tuned -- prefer high-level Table.merge with its slightly more conservative update;
|
file |
diff |
annotate
|
| Mon, 07 Jan 2013 22:21:56 +0100 |
wenzelm |
more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed;
|
file |
diff |
annotate
|
| Mon, 07 Jan 2013 11:59:37 +0100 |
wenzelm |
tuned comment -- do not claim anything;
|
file |
diff |
annotate
|
| Sat, 20 Aug 2011 23:35:30 +0200 |
wenzelm |
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 20:22:22 +0200 |
wenzelm |
tuned signature: Name.invent and Name.invent_names;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 14:05: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
|
| Sun, 17 Apr 2011 19:54:04 +0200 |
wenzelm |
report Name_Space.declare/define, relatively to context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|