| Fri, 16 Apr 2010 20:56:40 +0200 |
wenzelm |
allow syntax types within abbreviations;
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 19:43:06 +0200 |
wenzelm |
local type abbreviations;
|
file |
diff |
annotate
|
| Thu, 15 Apr 2010 20:31:21 +0200 |
wenzelm |
explicit ProofContext.check_tfree;
|
file |
diff |
annotate
|
| Thu, 15 Apr 2010 18:09:22 +0200 |
wenzelm |
replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo;
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 00:41:34 +0100 |
wenzelm |
support type arguments with sort constraints;
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 22:56:32 +0100 |
wenzelm |
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
|
file |
diff |
annotate
|
| Sat, 13 Mar 2010 14:41:37 +0100 |
wenzelm |
added typedecl_wrt, which affects default sorts of type args;
|
file |
diff |
annotate
|
| Thu, 11 Mar 2010 18:52:50 +0100 |
wenzelm |
actually apply morphism to binding;
|
file |
diff |
annotate
|
| Tue, 09 Mar 2010 23:32:13 +0100 |
wenzelm |
localized typedecl;
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 12:47:02 +0100 |
wenzelm |
separate structure Typedecl;
|
file |
diff |
annotate
|