| Fri, 16 May 2014 19:13:50 +0200 | blanchet | use 'simp add:' syntax in Sledgehammer rather than 'using' | changeset | files |
| Fri, 16 May 2014 19:13:50 +0200 | blanchet | silence methods even better | changeset | files |
| Fri, 16 May 2014 19:13:50 +0200 | blanchet | honor original format of conjecture or hypotheses in Z3-to-Isar proofs | changeset | files |
| 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 |
| Fri, 16 May 2014 09:19:15 +0200 | nipkow | new syntax for card, normalized spacing for # | changeset | files |