Re: [isabelle] Track sorry
On 07.04.2014 15:11, Makarius wrote:
> Above I propose two conceptually different ways to check some Isabelle
> (1) In the Prover IDE, using hypersearch to look at the concrete
> (2) In batch mode, by using knowledge about the LCF kernel works.
> When Lars says "This will only tell the user whether all theorems are
> valid" he seems to refer to (2), while ignoring (1) -- and the
> fantastic hypersearch tool of jEdit.
Hypersearch doesn't help when the theorem is declared as simp (or
similar). And building a transitive closure using hypersearch is cumbersome.
This archive was generated by a fusion of
Pipermail (Mailman edition) and