Just an aside: concerning »insert« and »add«, infix syntax would be desirable, e.g.
a `insert` X
a `add` M
similar to
Y \union Y
N + M
which would yield much more readable propositions, esp. wrt. associativity:
a `insert` b `insert` X = {a, b} \union X
vs.
insert a (insert b X) = {a, b} \union X
This is structurally similar to append and cons on lists:
x # y # xs = [x, y] @ xs
But so far I have seen any convincing symbolic notation for that for
sets or multisets.
Cheers,
Florian
--
PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
