| Sat, 28 Dec 2013 21:06:24 +0100 | haftmann | postpone dis"useful" lemmas | changeset | files |
| Sat, 28 Dec 2013 21:06:22 +0100 | haftmann | cleanup | changeset | files |
| Sat, 28 Dec 2013 17:51:54 +0100 | haftmann | prefix disambiguation | changeset | files |
| Fri, 27 Dec 2013 20:35:32 +0100 | haftmann | tuned proofs and declarations | changeset | files |
| Fri, 27 Dec 2013 14:35:14 +0100 | haftmann | prefer target-style syntaxx for sublocale | changeset | files |
| Thu, 26 Dec 2013 22:47:49 +0100 | haftmann | prefer ephemeral interpretation over interpretation in proof contexts; | changeset | files |
| Wed, 25 Dec 2013 22:35:29 +0100 | haftmann | self-contained formulation of subclass command, avoiding hard-wired Named_Target.init | changeset | files |
| Wed, 25 Dec 2013 22:35:28 +0100 | haftmann | ephemeral interpretation also formally works on theory level | changeset | files |