[isabelle-dev] Status of HOL/SMT

[Makarius]

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