Re: [isabelle-dev] Isabelle gets stuck when imported theory is not found
On Mon, 16 Mar 2015, Makarius wrote: On Mon, 16 Mar 2015, Makarius wrote: I have reworked this substantially in various changesets leading up to 5d0c539537c9. It is surprising how much time can be spent on such details. Now there is even some semantic completion, to propose a theory name that fits to the file name, in the error saying that there is a disagreement. A note to enthusiastioc testers: in the above version the 'theory' keyword needs to be right at the start of the file. It is presently a consequence of slightly odd mismatches of command spans vs. formal headers. I have reworked this in 5c1a0069b9d3 and c443ca40ef8d, so that the 'theory' keyword may be anywhere. Moreover the header format to determine the session graph dependencies and local syntax of each editor buffer is a bit more liberal. It remains to be seen in the coming weeks before the Isabelle2015 release if further details need to become more smooth. As usual, it is not immediately clear, how the system should react on partial or broken input during the continous editing process. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-Probability broken
Sorry, I overlooked this due to the many untracked files of the form *.prv. Wouldn’t it make sense to add this pattern to our .hgignore file? Larry > On 18 Mar 2015, at 14:52, Makarius wrote: > > On Tue, 17 Mar 2015, Larry Paulson wrote: > >> I’ve pushed a correction to that particular problem. > > That version f41a2f77ab1b looks fine. > > >> I’ve no time to verify that there are no further problems. Sorry again. > > New further problems emerge in 5b762cd73a8e: total existence failure due to > missing file Complex_Transcendental.thy. > > > Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-Probability broken
On Tue, 17 Mar 2015, Larry Paulson wrote: I’ve pushed a correction to that particular problem. That version f41a2f77ab1b looks fine. I’ve no time to verify that there are no further problems. Sorry again. New further problems emerge in 5b762cd73a8e: total existence failure due to missing file Complex_Transcendental.thy. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] New proof method "rewrite"
Hi, commit 4ed50ebf5d36 adds a new proof method "rewrite". This is the pattern-based replacement for subst Christoph Traut and I presented at the last Isabelle Workshop [1]. For now, it lifes in ~~/src/HOL/Library/Rewrite and is still missing a proper documentation (but there are examples in ~~/src/HOL/ex/Rewrite_Examples). The plan is to eventually move it into the main HOL image (although technically it should work with any logic with a simplifier setup). [1] https://www21.in.tum.de/~noschinl/Pattern-2014/ ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
