Peter and I minimized the last example:
ML‹
fun get_some var =
case Synchronized.value var of
NONE => (@{print} "defer"; get_some var)
| SOME v => (@{print} "got it"; v)
fun set var x =
Synchronized.change var (K x)
val thm: thm option Synchronized.var = Synchronized.var
On 06/13/2016 07:48 PM, Lars Hupel wrote:
* AFAIS, pushing to the Isabelle testboard still requires local access
> rights at TUM. Are there any fundamental impediments to lift this
> restriction?
Yes. I have been arguing that we should move the official Isabelle
repository to Bitbucket for a
As Andreas already mentioned, we've been consistently using the symbol
\Mapsto for ===> in our papers. Concerning --->, we used \mapsto.
Ondrej
On 03/04/2016 12:36 PM, Andreas Lochbihler wrote:
Hi Makarius,
How about LaTeX \Mapsto for ===>? This is what I use in my papers
following Ondrej
* Transfer:
- new methods for interactive debugging of 'transfer' and
'transfer_prover': 'transfer_start', 'transfer_step',
'transfer_end', 'transfer_prover_start'
and 'transfer_prover_end'.
This refers to 46af4f577c7e.
See the Isar Reference Manual and the example file
This is what I already did when I pushed the upgrade of the lifting
package. I contacted René Thiemann and proposed to make his AFP entry
empty except for a single file that would explain what happened.
As far as I can remember, he wasn't happy with this solution and
proposed to keep the
I also had a similar problem some time ago and I solved it by changing
the proof. You can get by bisecting to the very point that makes
HOL-Proofs choke and change it. I am not sure anymore but I think in my
example I just changed metis for blast or something like this.
Ondrej
On 05/13/2014
This refers to 682bba24e474.
If I have a theory file that contains a method that loops (use for
example lemma False by (intro FalseE)) and if I close this file in
JEdit, the method presumably still loops in the background. I have to
open the file again and edit it to stop the looping. Is this
Hi!
In the past couple of months I've gotten a crash of PolyML always with
the same error message. I cannot reproduce the problem reliably but
because it has already happened, let say, six times in the past three
months, I am reporting the problem here:
Unofficial version of Isabelle/HOL
On 09/11/2013 12:52 PM, Makarius wrote:
On Tue, 10 Sep 2013, Makarius wrote:
In the meantime I have tried a few keyboards that still have a numpad
-- they usually work with page or arrow movement, but not digits.
It needs further investigation to understand which of the fixes of
jEdit key
On 09/02/2013 12:21 PM, Makarius wrote:
On Fri, 30 Aug 2013, Makarius wrote:
These days a numpad is relatively rare on keyboards. (I have one at
the big laptop at home, but it has quite different behaviour than the
more regular numpads on old-style stand-alone keyboards.)
I have made some
On 08/30/2013 02:21 PM, Makarius wrote:
On Thu, 29 Aug 2013, Ondřej Kunčar wrote:
This refers to 3c26a7042d8e. The numpad stopped working in JEdit.
Reproducible on my machine and also on Dmitriy's machine. We use Linux.
What exactly means stopped working? Can you give another changeset where
This refers to 3c26a7042d8e. The numpad stopped working in JEdit.
Reproducible on my machine and also on Dmitriy's machine. We use Linux.
Ondrej
___
isabelle-dev mailing list
isabelle-...@in.tum.de
Dear Isabelle-Dev,
this refers to fbf4d50dec91.
Recently I started using interpretation in anonymous contexts to
introduce syntax locally. But now I noticed that print_theorems behaves
differently than I expected.
Consider this example:
context begin
interpretation lifting_syntax .
term op
Dear All,
this refers to 3fbcfa911863.
If I use the proof recording, processing of the following theory takes
infinite time:
theory Problem
imports Main
begin
lemma list_all2 (Lifting.invariant P) = Lifting.invariant (list_all P)
apply (simp add: fun_eq_iff list_all2_def list_all_iff
Hi!
Recently I noticed that it takes considerably more time to build
Isabelle (makeall) on testboard than it used to take before. I did a
small inspection and something must have happened between 25.3.2013 and
26.3.2013 because this build from 25.3. took 27 minutes
On 01/10/2013 01:25 PM, Jasmin Christian Blanchette wrote:
Am 10.01.2013 um 13:16 schrieb Jasmin Blanchette:
I just updated Isabelle to af8ecf09a58c (from a version that was one or two
days old) and whenever I try to build HOL, I get this error:
isabelle build -c -b HOL
Fehler:
On 11/08/2012 11:59 AM, Tobias Nipkow wrote:
This is exactly why I am against SMT certificates in AFP entries. Ondrej, can
you possibly remove them?
All SMT calls are now removed (changeset 3685878ce7b7).
But AVL-Trees were already broken in Isabelle's changeset 791157a4179a
(ensured that
On 10/20/2012 09:45 AM, Florian Haftmann wrote:
Hi Ondrej,
Hi Florian,
the changeset
http://isabelle.in.tum.de/reports/Isabelle/rev/70300f1b6835 broke the
AFP sessions JinjaThreads and KBPs.
Yes, I know. I already fixed Collections on Friday and I am going to go
back to this problem on
On 04/26/2012 02:09 PM, Makarius wrote:
The website itself is starting to take shape. Thanks to Johannes Hölzl
we now have nice download buttons that detect the platform of the web
browser: Linux, Linux 64 bit, Mac OS X, Windows. All 4 buttons are shown
if the platform cannot be detected.
After a long discussion during a lunch break we decided to use
.rep_eq. I will also change _rsp to .rsp. What about _def?
Should I change it to .def as well? _def seems to be a
inconsistency, I guess because of historical reasons. Should new
packages use .def instead of _def?
Ondrej
On
On 03/23/2012 05:34 PM, Makarius wrote:
Just a note on the following changeset:
changeset: 47095:3ea48c19673e
user: kuncar
date: Fri Mar 23 14:25:31 2012 +0100
files: src/HOL/Quotient.thy src/HOL/Tools/Quotient/quotient_def.ML
src/HOL/Tools/Quotient/quotient_term.ML
Hi!
I found out that the pretty-printer for terms in Isabelle do implicitly
beta-normalization and this behavior can't be turned off (in contrast to
eta-normalization).
Is there any serious reason why I can't turn off this feature like in
the case of eta-normalization? It's a bit annoying if
Hi!
It seems that the compilation of IsarRef is broken. I've got the
following error with the 45669:06e259492f6b changeset:
~/tmp/isabelle-dev/doc-src/IsarRef ../../bin/isabelle make
Running HOL-IsarRef ...
HOL-IsarRef FAILED
val CONTEXT_REWRITE_RULE :
term * term list * thm * thm list
23 matches
Mail list logo
