Re: [isabelle-dev] An experience report on the testboard

Hi Florian, thanks for your feedback! Commenting in some more detail will take me some time, but for now a quick reply: > 1. Changesets to dist and AFP exist as hg patches. This is currently not implemented. Isabelle testboard will always use AFP devel and vice versa. It is not possible to test

[isabelle-dev] Considered harmful: surj

Hi all, since cf26dd7395e4, ‹surj f› is a mere abbreviation for ‹range f = UNIV›. This is a little bit unfortunate since an ordinary equation is just hidden in output that way, resulting in lots of casual confusion. I would suggest to turn ‹surj› into a mere input abbreviation, similar to

[isabelle-dev] {0::nat..<n} = {..<n}

Hi all, obviously on natural numbers ‹{0..

[isabelle-dev] An experience report on the testboard

Hi all, I have started to use the testboard and want to excite feedback on my workflow, as well as hint to certain inconveniences in the current setup. 1. Changesets to dist and AFP exist as hg patches. 2. In both repositories: hg push_to_testboard where »push_to_testboard«