Re: [isabelle-dev] NEWS: limited name space accesses
On 07/04/2015 16:28, Makarius wrote: A real danger in the whole affair is that we need to proceed towards the Isabelle2015 release very soon, i.e. this week. Which in the past would have meant not to include the new concept. But maybe you want to set a precedent. Tobias smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Mira still alive?
On 02.04.2015 00:31, Makarius wrote: On http://isabelle.in.tum.de/reports/Isabelle there is very little to see. This is occasionally important to investigate timing problems, or to see how Isabelle vs. AFP works out. The testbench suites were running, but none of the other tests. One instance was even hanging since a last september. As I usually don't need these services, I only notice hiccups when somebody tells me about it. Unfortunately, mira is not very reliable. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Multiset insert
Sounds logical to me.
Larry
On 8 Apr 2015, at 08:13, Tobias Nipkow nip...@in.tum.de wrote:
Currently the setup in Multiset is geared towards having the 3 basic
(non-free) constructors: empty, singleton and union. Although induction
already has only two cases (empty and union with singleton), it would be
nicer to have only two constructors, like for finite sets: empty and insert.
In particular, this often avoids the use of ac_simps for union because
representations are more canonical. The singleton constructor would be
retained as an abbreviation for insert_mset _ {#} but M + {#x#} would be
simplified to insert_mset x M, like for sets.
Any views?
Tobias
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Multiset insert
Currently the setup in Multiset is geared towards having the 3 basic (non-free)
constructors: empty, singleton and union. Although induction already has only
two cases (empty and union with singleton), it would be nicer to have only two
constructors, like for finite sets: empty and insert. In particular, this often
avoids the use of ac_simps for union because representations are more canonical.
The singleton constructor would be retained as an abbreviation for insert_mset
_ {#} but M + {#x#} would be simplified to insert_mset x M, like for sets.
Any views?
Tobias
smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Multiset insert
The singleton constructor
would be retained as an abbreviation for insert_mset _ {#}
Maybe even that won't be necessary since there is also explicit
enumeration syntax for multisets, AFAIR.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.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
