Am 12.05.2014 um 23:10 schrieb Makarius :
> This sounds both a bit like "testing-unstable-HOL". But there is no problem
> to experiment with axiomatizations, if it clear to the user what it is, and
> not a seamingly harmless "bnf_decl".
For the record: The name "bnf_decl" was modeled after "ty
On Mon, 12 May 2014, Dmitriy Traytel wrote:
There are two classes of users for bnf_decl:
the Popescu-class:
Anybody who would like to be able to quantify over type constructors
in HOL in order to reason abstractly.
the Traytel-class:
Any developer of extensions to the BNF machinery. He
Am 12.05.2014 16:54, schrieb Makarius:
This is a continuation of the thread: "code_pred" introduces axioms?
(October / November 2013).
Back then, on Thu, 31 Oct 2013, Andreas Lochbihler wrote:
When Lukas told me about the axioms about three years ago, he said
that indeed these axioms only spe
The list of remaining uses of Proof General is shrinking dramatically
every day. We can continue this a bit more during May, all referring to
ongoing repository development.
During the month of June, I will be mostly on vacation. After that the
convergence towards the release needs to start.
> 1. Violation of well-sortedness constraints: type ... not an instance of
> ...
>
> declare [[show_sorts]]
> code_thms
>
> Then, I use educated guessing and Emacs' incremental search to navigate
> the code equations that have been output until I find the fault --
> usually, it's just a missing
This is a continuation of the thread: "code_pred" introduces axioms?
(October / November 2013).
Back then, on Thu, 31 Oct 2013, Andreas Lochbihler wrote:
When Lukas told me about the axioms about three years ago, he said that
indeed these axioms only specify new constants which the inductify
On Thu, 8 May 2014, David Matthews wrote:
On 08/05/2014 11:25, Makarius wrote:
That sounds rather obvious, but also like even more complication.
David Matthews has provided a nice simplified version of pthreads in
Poly/ML. He could probably do more, but even on the more complex JVM
the inf
On Tue, 29 Apr 2014, Thomas Sewell wrote:
Back to the actual technical questions. What are the main performance
bottle-necks here? Printing of intermediate goal states? Or applying
intermediate steps repeatedly?
I suspect that the problem is not that the printing or the intermediate
calc
On Fri, 2 May 2014, Makarius wrote:
On Tue, 29 Apr 2014, Andreas Lochbihler wrote:
Until then there are various approximations:
* Multiple floating instances of Output, with different Update / Auto
update state.
* The Output / Detach button to produce an unchanging Info window on the
* Improved management of dockable windows: clarified keyboard focus
and window placement wrt. main editor view; optional menu item to
"Detach" a copy where this makes sense.
This refers to Isabelle/c2ddbf327bbd.
After the docking framework of jEdit came up again in recent discussions
on this m
On Mon, 12 May 2014, Tjark Weber wrote:
On Fri, 2014-05-09 at 12:00 +0200, Tjark Weber wrote:
Moreover, it is merely a historic accident that the theory is based on
Refute. [...]
I am attaching a patch that replaces Refute with Nitpick in
HOL/ex/Sudoku.thy.
Thanks. I have pushed this as Is
11 matches
Mail list logo
