Fri, 16 May 2014 12:56:39 +0200 | blanchet | proper handling of 'ctor_dtor' for mutual corecursive cases where not all type variables are present in all low-level constructors (cf. 'coind_wit1' etc. in 'Misc_Codatatypes.thy') | changeset | files |
Fri, 16 May 2014 09:19:15 +0200 | nipkow | new syntax for card, normalized spacing for # | changeset | files |
Thu, 15 May 2014 16:46:29 +0200 | haftmann | clarified stylized status of sandwich algebra | changeset | files |
Thu, 15 May 2014 16:38:33 +0200 | haftmann | dropped dead code | changeset | files |
Thu, 15 May 2014 16:38:32 +0200 | haftmann | accurate separation of static and dynamic context | changeset | files |
Thu, 15 May 2014 16:38:31 +0200 | haftmann | syntactic means to prevent accidental mixup of static and dynamic context | changeset | files |
Thu, 15 May 2014 16:38:31 +0200 | haftmann | proper separation of static and dynamic context | changeset | files |
Thu, 15 May 2014 16:38:30 +0200 | haftmann | optimization for trivial cases | changeset | files |