| Fri, 16 May 2014 17:11:56 +0200 | wenzelm | proper priority for error over warning, which got mixed up in 0546e036d1c0 and 4df2727a0b5f; | changeset | files |
| Fri, 16 May 2014 16:40:02 +0200 | noschinl | added lemmas for -1 | changeset | files |
| 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 |