| 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 |
| Wed, 25 Dec 2013 17:39:07 +0100 | haftmann | abolished slightly odd global lattice interpretation for min/max | changeset | files |
| Wed, 25 Dec 2013 17:39:06 +0100 | haftmann | prefer more canonical names for lemmas on min/max | changeset | files |
| Wed, 25 Dec 2013 17:39:06 +0100 | haftmann | explicit distributivity facts on min/max | changeset | files |
| Wed, 25 Dec 2013 15:52:25 +0100 | haftmann | postponed min/max lemmas until abstract lattice is available | changeset | files |