| Sat, 13 Mar 2010 14:44:47 +0100 | wenzelm | adapted to localized typedef: handle single global interpretation only; | changeset | files |
| Sat, 13 Mar 2010 14:43:04 +0100 | wenzelm | global typedef; | changeset | files |
| Sat, 13 Mar 2010 14:42:16 +0100 | wenzelm | localized typedef; | changeset | files |
| Sat, 13 Mar 2010 14:41:37 +0100 | wenzelm | added typedecl_wrt, which affects default sorts of type args; | changeset | files |
| Sat, 13 Mar 2010 14:41:14 +0100 | wenzelm | Local_Defs.contract convenience; | changeset | files |
| Sat, 13 Mar 2010 14:40:36 +0100 | wenzelm | added Local_Theory.alias operations (independent of target); | changeset | files |
| Thu, 11 Mar 2010 23:47:16 +0100 | wenzelm | merged | changeset | files |
| Thu, 11 Mar 2010 19:06:03 +0100 | nipkow | merged | changeset | files |
| Thu, 11 Mar 2010 19:05:46 +0100 | nipkow | converted proofs to Isar | changeset | files |
| Thu, 11 Mar 2010 17:52:15 +0100 | haftmann | merged | changeset | files |
| Thu, 11 Mar 2010 17:39:45 +0100 | haftmann | merged | changeset | files |
| Thu, 11 Mar 2010 15:52:35 +0100 | haftmann | tuned prefix of ac rules | changeset | files |
| Thu, 11 Mar 2010 15:52:35 +0100 | haftmann | deleted default simp rule card.insert | changeset | files |
| Thu, 11 Mar 2010 15:52:34 +0100 | haftmann | updated generated certificate | changeset | files |
| Thu, 11 Mar 2010 15:52:34 +0100 | haftmann | replaced card_def by card_eq_setsum | changeset | files |
| Thu, 11 Mar 2010 15:52:33 +0100 | haftmann | NEWS | changeset | files |
| Thu, 11 Mar 2010 14:40:29 +0100 | haftmann | Big_Operators now in Main rather than Plain | changeset | files |
| Thu, 11 Mar 2010 14:39:58 +0100 | haftmann | tuned prefixes of ac interpretations | changeset | files |
| Thu, 11 Mar 2010 14:39:58 +0100 | haftmann | Big_Operators now in Main rather than Plain src/HOL/Wellfounded.thy | changeset | files |
| Thu, 11 Mar 2010 14:38:20 +0100 | haftmann | fixed typo | changeset | files |
| Thu, 11 Mar 2010 14:38:19 +0100 | haftmann | tuned monoid locales and prefix of sublocale interpretations | changeset | files |
| Thu, 11 Mar 2010 14:38:13 +0100 | haftmann | moved cardinality to Finite_Set as far as appropriate; added locales for fold_image | changeset | files |
| Thu, 11 Mar 2010 14:38:09 +0100 | haftmann | fixed typo | changeset | files |
| Wed, 10 Mar 2010 16:53:43 +0100 | haftmann | added locales for monoids | changeset | files |
| Wed, 10 Mar 2010 16:53:27 +0100 | haftmann | split off theory Big_Operators from theory Finite_Set | changeset | files |
| Thu, 11 Mar 2010 17:48:07 +0100 | blanchet | moved some Nitpick code around | changeset | files |
| Thu, 11 Mar 2010 23:45:41 +0100 | wenzelm | more basic Local_Defs.export_cterm; | changeset | files |
| Thu, 11 Mar 2010 23:07:12 +0100 | wenzelm | tuned signature; | changeset | files |
| Thu, 11 Mar 2010 23:07:02 +0100 | wenzelm | tuned; | changeset | files |
| Thu, 11 Mar 2010 18:52:50 +0100 | wenzelm | actually apply morphism to binding; | changeset | files |