> but this leads to the rather lengthy "insert_mset x M" as opposed to the
> current "{#x#} + M". This would come up in all inductive proofs. If we want
> to mimic sets, it actually seems unavoidable...
With completion, it might actually be easier to type "insert_mset x M" than
"{#x#} + M".
On 10/03/2016 11:00, Florian Haftmann wrote:
Hi all,
traditionally, syntax for lattice operations (⊓ ⊔ ⊥ ⊤ etc.) has been
kept in a separate library theory, to allow use of that quite generic
notation for unforeseen applications.
Meanwhile however all those operations to which
Although I suggested we do this, and still think logically it is the right thing
to do, I see one issue, the naming of insert#. The canonical name is
insert_mset, but this leads to the rather lengthy "insert_mset x M" as opposed
to the current "{#x#} + M". This would come up in all inductive
Hi all,
the attached patches (based on f26dc26f2161) sketch how a generic
interval [_..<_] / [_.._] could look like in List.thy.
Key points:
* The required logical properties are obtained by a specialization of
linordered_semidom with
a <= b <--> (EX n. b = a + of_nat n)"
This avoids
