| Tue, 23 Aug 2011 03:34:17 +0900 |
Cezary Kaliszyk |
Quotient Package: some infrastructure for lifting inside sets
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Fri, 07 Jan 2011 21:26:49 +0100 |
wenzelm |
do not open ML structures;
|
file |
diff |
annotate
|
| Fri, 07 Jan 2011 15:35:00 +0100 |
wenzelm |
more precise parentheses and indentation;
|
file |
diff |
annotate
|
| Thu, 28 Oct 2010 22:11:06 +0200 |
wenzelm |
handle Type.TYPE_MATCH, not arbitrary exceptions via MATCH_TYPE variable;
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 10:56:46 +0200 |
haftmann |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 20:04:49 +0800 |
Christian Urban |
tuned code
|
file |
diff |
annotate
|
| Tue, 24 Aug 2010 22:38:45 +0800 |
Christian Urban |
use matching of types than just equality - this is needed in nominal to cope with type variables
|
file |
diff |
annotate
|
| Sun, 22 Aug 2010 10:45:53 +0800 |
Christian Urban |
changed to a more convenient argument order
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 16:08:59 +0200 |
haftmann |
tuned quotes
|
file |
diff |
annotate
|
| Thu, 08 Jul 2010 16:19:24 +0200 |
haftmann |
tuned titles
|
file |
diff |
annotate
|
| Thu, 01 Jul 2010 16:54:42 +0200 |
haftmann |
qualified constants Set.member and Set.Collect
|
file |
diff |
annotate
|
| Tue, 29 Jun 2010 09:37:23 +0100 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
| Mon, 28 Jun 2010 16:20:39 +0100 |
Christian Urban |
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
|
file |
diff |
annotate
|