Re: [isabelle] Track sorry



On 07.04.2014 15:11, Makarius wrote:
>
> Above I propose two conceptually different ways to check some Isabelle
> development;
>
>   (1) In the Prover IDE, using hypersearch to look at the concrete
> syntax.
>
>   (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.

  -- Lars




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.