On Tue, 7 Apr 2015, Makarius wrote:
On Tue, 7 Apr 2015, Tobias Nipkow wrote:
On 07/04/2015 14:37, Christian Sternagel wrote:
(b) qualified
That gets my vote because it expresses clearly the description Makarius
gave: name space entry that is only accessible by qualified names
It is
Hi Andreas,
In Isabelle2014, processing this datatype declaration takes about one minute.
So what has happened in between? (The Isabelle2014 timing panel is also way
off with 8 seconds.)
Thanks for your report. What happened in between is that we generate more
theorems. I suspect one or a
Dear BNF and Isabelle/jEdit developers,
Today, I noticed that the datatype command in Isabelle/e936c2828bec is sometimes extremely
slow. At the end of this mail, there is a large enumeration type where this shows up.
Processing this definition on my laptop takes about 4 minutes, but the timing
Hi Andreas,
rather than going dirty, try:
datatype (plugins only:) family ...
It seems that here we are lucky and the slowdown is caused by one of
the plugins. (We'll investigate which one.)
Cheers,
Dmitriy
PS: Your datatype reminded me of another one, which allows (or allowed)
proving
* Local theory specification commands may have a 'private' or 'qualified'
modifier to restrict name space accesses to the local scope, as provided
by some context begin ... end block. For example:
context
begin
private definition ...
private lemma ...
qualified definition ...
On Wed, 8 Apr 2015, Jasmin Blanchette wrote:
- Z3 is now always enabled by default, now that it is fully open
source. The z3_non_commercial option is discontinued.
In addition, Z3 should now (again) be invoked by default by
Sledgehammer. Let me know if you see anything odd, e.g. odd
This is the start of the thread for the hot phase. Until lift-off it can
take 6-12 weeks. More precise announcements of events of the preparation
phase will come within the next few days.
Right now we still have a couple of days of regular changes on the
repository. This is also an
On Thu, 9 Apr 2015, Lars Noschinski wrote:
On 18.03.2015 15:16, Lars Noschinski wrote:
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
Hi Dmitriy and Jasmin,
Thanks for the hint with plugins. That really speeds things up. I also suspect that the
timing panel does not include the forked proof tactics.
Cheers,
Andreas
On 09/04/15 15:55, Dmitriy Traytel wrote:
Hi Andreas,
rather than going dirty, try:
datatype (plugins
Can you explain the status of Old_SMT? Is there anything that isatest still
needs to run here?
“old_smt” is there just in case. I was thinking of killing it right after the
Isabelle2015 release. It’s not even tested by any regression test. People like
Filip Maric, who use Z3 heavily (cf.
On 18.03.2015 15:16, Lars Noschinski wrote:
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
11 matches
Mail list logo
