On Tue, 4 Dec 2012, Gerwin Klein wrote:
I've done this recently for several other sessions where that was
"forgotten", e.g. Sum_of_Squares and the skip_proofs flag. (For
WWW_Find I don't know how to do that, so it remains untested and broken
for now.)
Tim is looking at WWW_Find, but he's in the process of moving to France,
so there might be a few delays.
WWW_Find is not a session as such, though, so I'm not sure why it
becomes relevant here. It should just work from an existing image and
not do any proofs itself on top.
It is off-topic for SMT, but one of the examples for "forgotten" tests.
Anyting that is not automatically checked by one of our little agents in
the background will rot very soon. This is relevant now, as we are moving
towards the next official release of everything.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
