| Thu, 12 Aug 2010 20:11:13 +0800 |
Christian Urban |
simplified code
|
file |
diff |
annotate
|
| Thu, 08 Jul 2010 16:19:24 +0200 |
haftmann |
tuned titles
|
file |
diff |
annotate
|
| Thu, 24 Jun 2010 12:33:51 +0100 |
Christian Urban |
export of proper information in the ML-interface of the quotient package
|
file |
diff |
annotate
|
| Wed, 23 Jun 2010 08:44:44 +0200 |
Cezary Kaliszyk |
Quotient package now uses Partial Equivalence instead place of equivalence
|
file |
diff |
annotate
|
| Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 15:52:03 +0200 |
wenzelm |
modernized naming conventions of main Isar proof elements;
|
file |
diff |
annotate
|
| Sat, 27 Mar 2010 21:38:38 +0100 |
wenzelm |
Typedef.info: separate global and local part, only the latter is transformed by morphisms;
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 00:47:23 +0100 |
wenzelm |
typedef etc.: no constraints;
|
file |
diff |
annotate
|
| Tue, 16 Mar 2010 08:45:08 +0100 |
Christian Urban |
rollback of local typedef until problem with type-variables can be sorted out; fixed header
|
file |
diff |
annotate
|
| Sun, 14 Mar 2010 15:50:17 +0100 |
Christian Urban |
removed Local_Theory.theory_result by using local Typedef.add_typedef
|
file |
diff |
annotate
|
| Sun, 14 Mar 2010 14:31:24 +0100 |
wenzelm |
observe standard header format;
|
file |
diff |
annotate
|
| Sat, 13 Mar 2010 14:43:04 +0100 |
wenzelm |
global typedef;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 12:30:55 +0100 |
Cezary Kaliszyk |
export add_quotient_type.
|
file |
diff |
annotate
|
| Wed, 24 Feb 2010 20:37:01 +0100 |
wenzelm |
allow general mixfix syntax for type constructors;
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 13:54:19 +0100 |
Cezary Kaliszyk |
Initial version of HOL quotient package.
|
file |
diff |
annotate
|