Hi Makarius,
> On 1 Jun 2018, at 23:32, Makarius wrote:
>
> On 01/06/18 10:35, Dmitriy Traytel wrote:
>> Hi all,
>>
>> thanks for pointing this out, Lars. And thanks for looking at the sources,
>> Jasmin.
>>
>> The problem seems to only show
Hi all,
thanks for pointing this out, Lars. And thanks for looking at the sources,
Jasmin.
The problem seems to only show up when the declaration in question is inside of
a class context. Here is a reduced version that does not involve primrec at all.
context linorder begin
context fixes b ::
Hi Larry,
in ~~/src/HOL/ROOT, the theory Probability is declared as "global". That means
that you must import it without any session qualification (just like Main or
Complex_Main).
Dmitriy
> On 2 Nov 2017, at 17:47, Lawrence Paulson wrote:
>
> I’ve been converting some theories from the old
Hi Lars,
thanks for the reminder. Cf. c6714a9562ae and a5a24e1a6d6f.
Note that this still doesn’t provide the interface to Lifting and Transfer via
transfer rules for the BNF constants (which is more complicated since lift_bnf
doesn’t know about Lifting, in particular about the correspondence r
Hi Makarius,
> On 24 Apr 2017, at 18:12, Makarius wrote:
>
> On 24/04/17 14:46, Makarius wrote:
>>
>> Are there users of it outside the TUM group?
My usage is the same as in Jasmin’s and Andreas’ case.
>>
>> What is good about it? What is bad about it?
>
> (1) To follow the line of Mira vs.
Hi Makarius,
> On 10 May 2016, at 22:48, Makarius wrote:
>
> On 03/03/16 14:19, Dmitriy Traytel wrote:
>
>> I wondered whether named_theorems (or more generally all dynamic facts)
>> deserve to be more visible. In particular when I search for
>>
>>
Hi Makarius,
this is nice. At first I was a bit surprised to see the first occurrence of
list, Nil, and Cons in blue in the following datatype definitions.
datatype 'a list = Nil | Cons 'a "'a list”
But I guess, it makes sense to indicate that this is a new thing being defined.
The question is
Hi Lars,
thanks for your work. Unfortunately, currently pushing to testboard/isabelle
does not seem to trigger new builds. Is this related to the job renamings?
Another renaming issue is visible here:
https://ci.isabelle.systems/status/
The status icon still points to (the now non-existent) is
> On 05 Mar 2016, at 23:11, Makarius wrote:
>
> *** ML ***
>
> * Local_Theory.restore has been renamed to Local_Theory.reset to
> emphasize its disruptive impact on the cumulative context, notably the
> scope of 'private' or 'qualified' names. Note that Local_Theory.reset is
> only appropriate
Hi all,
trying the smaller audience of isabelle-dev first.
I wondered whether named_theorems (or more generally all dynamic facts) deserve
to be more visible. In particular when I search for
"(?a < ?c - ?b) = (?a + ?b < ?c)”
with find_theorems, I’d like to be reminded of algebra_simps
Maybe a guess in the blue, but here is what grep tells me:
~$ grep base_name ~/isabelle/src/HOL/Tools/ -r | grep Quick
/Users/traytel/isabelle/src/HOL/Tools//Quickcheck/abstract_generators.ML:
val name = Long_Name.base_name tyco
I have not investigated further.
Dmitriy
> On 27 Feb 2016, at
Hi Lars,
yes, I also saw this on testboard and was confused.
On my (low-end 2 core) machine (isabelle/e4e09a6e3922, afp/123d7cbae549):
~/repos/nonprim-corec/paper$ isabelle build -vd '$AFP' Formula_Derivatives
ISABELLE_BUILD_OPTIONS="threads=4 parallel_proofs=2"
ISABELLE_BUILD_JAVA_OPTIONS="-Dj
Hi Lars,
even without the slow sessions, this is of great help. Thanks!
My commit yesterday (isabelle/ae44f16dcea5) broke some AFP entries (because
without the afp_testboard, I used to follow the "break it, fix it” philosophy
w.r.t. AFP). I will repair those today.
Dmitriy
> On 17 Feb 2016, a
> On 16 Feb 2016, at 11:30, Makarius wrote:
>
> On Tue, 16 Feb 2016, Dmitriy Traytel wrote:
>
>> I am unsure if an Isabelle tool is the right level of abstraction for an
>> operation, only members of the isabelle (UNIX) group at TUM can/should
>> execute.
&g
Hi Lars,
I am unsure if an Isabelle tool is the right level of abstraction for an
operation, only members of the isabelle (UNIX) group at TUM can/should execute.
Also, wouldn’t a push to a fresh repository take quite long. (OK, negligible
compared to the actual build, but still.) And one still
Hi Lars,
great to hear!
What about having an additional afp_testboard repository where one could also
push -f changes. I am particularly interested in “slow” sessions there.
Thanks for your work,
Dmitriy
> On 30 Jan 2016, at 12:51, Lars Hupel wrote:
>
> Dear list,
>
> I'm currently performi
Hi Makarius,
here is one way to still (e1e6bb36b27a) edit the output buffer: to use the
compose key.
On my Mac, if I place the cursor into the output buffer and press alt-u
followed bei u, an ü appears in the output.
Dmitriy
> On 04 Nov 2015, at 20:42, Makarius wrote:
>
> On Wed, 4 Nov 2015
Hi Lars,
this was exactly the vision for copy_bnf, modulo that I thought of using a
plugin (“src/Pure/Tools/plugin.ML”) instead of an option. But since I am not
the author of record, I went for the less invasive option of a separate command
(in the spirit of setup_lifting for typedef). So if th
Those look to me as if they have to do with 2314c2f62eb1 (real_of_nat_Suc is
now a simprule). Verified only for the Integral.thy failure.
Dmitriy
> On 06 Oct 2015, at 23:19, Makarius wrote:
>
> Here are some more proof failures (Isabelle/5b5656a63bd6 and
> AFP/21bdf9fbf229):
>
> Integration
As a data point: when testing 8d40ddaa427f I could build “HOL-Proofs” in about
17 minutes.
Timing = :threads=4elapsed=979.269cpu=2582.077gc=323.518factor=2.64
Dmitriy
> On 06 Oct 2015, at 21:54, Jasmin Blanchette
> wrote:
>
> Hi Makarius,
>
>> My impression is that ebf296fe88d7 (blan
Hi,
I’m not sure if this is rather something for the jEdit mailing list, but I try
here first. The attached theory is an empty 500+ lines long file where
everything is normal. However, if I add one new line the scrollbar disappears.
The above applies to 2007ea8615a2 but I believe I saw this beh
The title says it all.
Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
) = f« prints as »curry (λ(x, y). f
x y) = f« by default.
Any headache with this?
Florian
Am 10.09.2015 um 12:19 schrieb Dmitriy Traytel:
Hi Florian,
while I very much welcome the simplified printing rules and your effort
of unifying case_prod/split, I am not sure if adding a third
Hi Florian,
while I very much welcome the simplified printing rules and your effort
of unifying case_prod/split, I am not sure if adding a third alternative
name is the way to go. The situation reminds me of the one depicted in [1].
Clearly, case_prod is the "right" name from the perspective
Hi Florian,
On 27.08.2015 10:03, Florian Haftmann wrote:
Hi Dmitriy,
In short, I have come to the conclusion that
let (a, b) = p in t
case p of (a, b) => t
at the moment being logically distinct, should be one and the same. In
other words, I suggest that any case expression on tuples
On 19.08.2015 22:45, Makarius wrote:
On Wed, 19 Aug 2015, Larry Paulson wrote:
I pushed a changeset to the testboard, but it isn’t showing up at
http://isabelle.in.tum.de/testboard/Isabelle
The last change it shows was 6 days ago.
Moreover, testboard and the default branch look identical (I’
Oops, I didn't expect my name to appear here ;-)
The changeset 894d6d863823 was a reaction to Andreas Lochbihler's report
[1]. With turned off proofs the effect was a good one.
What is special about Pure.conjunction w.r.t. proof reconstruction? Is
it something in Goal.conjunction_tac? Would y
You can hover in the output panel, but you won't see types of constants
there.
Dmitriy
On 24.06.2015 16:09, Manuel Eberl wrote:
Ah, I see the problem. In that case, one could still hover over the
"of_nat" in the output window, but it is perhaps not ideal.
On 24/06/15 16:08,
I guess what Larry means is there is no way to see a type of a constant
that is not there in the source.
Consider e.g.
declare [[coercion "of_nat :: nat ⇒ real"]]
term "sqrt (2 :: nat)"
Today the output says "sqrt (real_of_nat 2)". But if there would be no
abbreviation for "of_nat :: nat ⇒ re
Hi,
I could not believe that recdef could not be replaced by fun, so here is
the patch that removes usages of recdef from Decision_Procs. The proof
rules that come out of the function package are fine (one just needs a
few split_format (complete) attributes in a few places).
I'm not sure if
Hi Florian,
On 06.06.2015 17:11, Florian Haftmann wrote:
The reason for the continued existence of recdef is that function can
cause a combinatorial explosion the way it compiles pattern matches. I
just tried Cooper.thy and changing one of the recdefs to function makes
Isabelle go blue (purple)
reas
On 13/04/15 12:04, Dmitriy Traytel wrote:
Hi Andreas,
I've investigated this a bit and the slowdown happens in the code
plugin in the
instantiation of the equal type class (i.e. datatype (plugins del:
code) is more precise
than the advice below). The number of theorems proved ther
forked proof tactics.
Cheers,
Andreas
On 09/04/15 15:55, Dmitriy Traytel wrote:
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.
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 F
Hi Makarius,
thanks, this is the hint I was looking for a long time now.
I will do the replacement in the BNF package, but I don't think that I
will have time for it before the approaching release.
Dmitriy
On 07.04.2015 17:47, Makarius wrote:
Just a short note on Local_Theory.open_target (f
Hi Makarius,
On 10.02.2015 18:30, Makarius wrote:
On Tue, 4 Nov 2014, Makarius wrote:
Strange hacks that work around the absence of proper options encumber
the introduction of them eventually. It is the usual bootstrap
problem for reforms.
I actually did start some work in the vicinity of r
mmand will show True (=the expected output with show_variants
= true), whereas T is expected with show_variants = false.
Cheers,
Dmitriy
On 28.01.2015 10:40, Dmitriy Traytel wrote:
Hi Chris,
I've pushed it to the testboard (and will push it to the repository in
case of succes
Hi Chris,
I've pushed it to the testboard (and will push it to the repository in
case of success):
http://isabelle.in.tum.de/testboard/Isabelle/rev/0d7de4d99eac
Cheers,
Dmitriy
On 28.01.2015 09:55, Christian Sternagel wrote:
It is amazing how easy some things get when a wizard is looking ove
Maybe then the timeout for AODV should be set to some large number in
its ROOT file (as done for other sessions)?
The session times out in mira for quite some time (e.g.
http://isabelle.in.tum.de/testboard/Isabelle/report/207ba9b7301d47a1a42585afb63c6a60).
Dmitriy
On 26.11.2014 22:31, Gerwin
obtained type-unifier to "v" and insert the
result instead of "c".
I hope this resolves your problem Andreas.
I tested the change on one of my local files that make heavy use of
adhoc overloading. Maybe someone could have a look, push the changes
to a test server, and pus
On 21.11.2014 15:00, Christian Sternagel wrote:
Hi Dmitriy,
thanks for another round of clarification (I should really reread old
emails before referring to them).
On 11/21/2014 02:43 PM, Dmitriy Traytel wrote:
In general, why not create map-functions that allow to map over *all*
type
e_HOL)
When we last brought up this point, Dmitriy suggested that users that
use "dead" in their datatypes know what they are doing and that it is
not a problem when packages "break" on such types. However, in IsaFoR
we sometimes kill type parameters just because otherwis
Sorry for reviving an ancient thread, but have the constants defined by
inductive ever been visible to find_consts since Florian's commit (I
presume 4a3747517552 ?).
Today in be4a911aca71 (but also in Isabelle2014 and even in
Isabelle2012) in the following
inductive xyz :: bool where "xyz"
f
http://isabelle.in.tum.de/reports/Isabelle/report/60d6105dac94411c8f55ea7626a15c71
anybody taking care of this?
Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
iously too hasty to remove
the test which exposed this time leak. Once this issue has been fixed,
I will put the "long" test back in, with a better comment.
Tobias
On 07/11/2014 15:27, Dmitriy Traytel wrote:
This is in Isabelle2014. In 229765cc3414 I make the same measurements
as Larry
This is in Isabelle2014. In 229765cc3414 I make the same measurements as
Larry. So indeed (as the text above those lemmas suggests) there seems
to be a regression with the simplifier setup.
Dmitriy
On 07.11.2014 15:10, Julian Brunner wrote:
The proof that 97 is prime only takes 1.3s on my mac
Yes, that's my bad. Thanks! I was about to check Mira for complaints.
See now AFP/ 1dd93cc85dfb.
Dmitriy
On 23.10.2014 14:25, Florian Haftmann wrote:
Isabelle 06dfbfa4b3ea
AFP 33c18a9138e9
*** Unknown old-style datatype "Regular_Exp.rexp"
*** At command "derive" (line 18 of
"/mnt/home/haftman
Antiquotations---bringing dependent types into Isabelle/ML :-)
This is really nice, Makarius. Thanks!
Dmitriy
On 08.10.2014 20:46, Makarius wrote:
*** ML ***
* Basic combinators map, fold, fold_map, split_list are available as
parameterized antiquotations, e.g. @{map 4} for lists of quadruple
On 17.09.2014 11:40, Jasmin Christian Blanchette wrote:
There are only a handful of "old_datatype"s left in the AFP, and they will go
away as soon as Dmitriy gets a chance to fix a bug in his code (presumably once he's back
from vacation).
It is now (isabelle/7b92932ffea5) fixed, and the "old_d
Indeed. Could the same be done for locales?
Dmitriy
On 10.09.2014 10:51, Tobias Nipkow wrote:
Florian showed it to me and class_deps has become really usable. I recommend
it to anyone out there in the class jungle.
Tobias
On 10/09/2014 10:49, Florian Haftmann wrote:
* Command "class_deps" ta
Hi Chris,
Am 05.09.2014 um 12:27 schrieb Christian Sternagel:
[...]
First question: is this intentional and what is the current default rule?
Yes. Quoting from the news:
The rule "set_cases" is now registered with the "[cases set]"
attribute. This can influence the behavior of the "c
On 03.07.2014 13:57, Peter Lammich wrote:
Hi,
I recently ran into a method that produced a stack-overflow.
The good thing is: In the current jedit version, it is properly
highlighted and you immediately see that there is some error. (This was
not always the case in the past)
The bad thing: The
Hi René,
this is a tactic failure in the recent size extension (the interface
with fun). We will work on it.
Thanks for the report,
Dmitriy
On 25.06.2014 13:49, René Thiemann wrote:
Dear all,
I have an unexpected problem when defining a datatype using datatype_new.
theory Test
imports
"
richt
Betreff: [isabelle] New AFP entry: Decision Procedures for MSO on Words
Based on Derivatives of Regular Expressions
Datum: Thu, 12 Jun 2014 22:35:58 +0200
Von:Tobias Nipkow
An: Isabelle Users
Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
Dm
Am 26.05.2014 12:53, schrieb Makarius:
On Mon, 26 May 2014, Dmitriy Traytel wrote:
Just on the squiggles in isolation: if these are rare add-on
options one
could invent long / explicit keywords for them (or Parse.literal
items).
grep gives 371 occurences of "-:" in IsaFoR
Am 26.05.2014 12:25, schrieb Makarius:
On Sun, 25 May 2014, Jasmin Christian Blanchette wrote:
The "=" as the name for Nil's discriminator deserves an explanation.
[...] So I introduced this weird "=" syntax, which suggests that
equality is used for discriminating. I am open to other suggestio
Am 26.05.2014 11:46, schrieb Tobias Nipkow:
On 26/05/2014 11:07, Jasmin Blanchette wrote:
Am 26.05.2014 um 11:02 schrieb Tobias Nipkow :
The definition of list should look like before.
I don't see how this is an option. This would result in the following duplicate
constants:
map_list
Am 26.05.2014 11:07, schrieb Jasmin Blanchette:
Am 26.05.2014 um 11:02 schrieb Tobias Nipkow :
The definition of list should look like before.
I don't see how this is an option. This would result in the following duplicate
constants:
map_list vs. map
set_list vs. set
rel_list
Am 13.05.2014 08:09, schrieb Jasmin Christian Blanchette:
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".
Fo
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
Could it be the document preparation?
Dmitriy
Am 05.05.2014 11:17, schrieb Johannes Hölzl:
Has anybody an idea why the AFP test for Probabilistic_Noninterference
fails?
When I build it on my machine with either the combination in the email
(i.e. AFP acd2cc051b4f and Isabelle 52e5bf245b2a) or a
Am 31.03.2014 23:14, schrieb Makarius:
On Fri, 28 Feb 2014, Makarius wrote:
I've made another round of refinements (presently at
Isabelle/f7ceebe2f1b5). There were some situations where the change
propagation of blobs (auxiliary files) versus theories was not right,
leading to an invalid pers
Am 14.03.2014 13:36, schrieb Makarius:
What is the status of the set_comprehension_pointfree simproc?
In 31afce809794 Dmitriy says "set_comprehension_pointfree simproc
causes to many surprises if enabled by default", and in 4d899933a51a
I've tried to reconstruct the missing NEWS entry, since
Am 18.02.2014 17:36, schrieb Dmitriy Traytel:
[...] Maybe I just hat too many ML files open (I usually don't close
them once opened) [...]
An addition: When I close an ML file, why does it need to be reloaded?
Dmitriy
___
isabelle-dev mailing
Hi Makarius,
Am 17.02.2014 14:14, schrieb Makarius:
* Improved support for Isabelle/ML, with jEdit mode "isabelle-ml" for
auxiliary ML files.
This refers to Isabelle/56ebc4d4d008. It continues recent
improvements of auxiliary file support.
The IDE support for Isabelle/ML is already quite s
Am 13.02.2014 13:08, schrieb Dmitriy Traytel:
Am 13.02.2014 12:48, schrieb Makarius:
Today isatest has reported a breakdown of HOL/Library/Code_Prolog.thy.
This was undetected in a more regular test due to this change that
removed it from the normal HOL-Library session:
changeset: 38504
Am 13.02.2014 12:48, schrieb Makarius:
Today isatest has reported a breakdown of HOL/Library/Code_Prolog.thy.
This was undetected in a more regular test due to this change that
removed it from the normal HOL-Library session:
changeset: 38504:76965c356d2a
user:haftmann
date:W
Should be fine again (or at least better) with b445c39cc7e9. Thanks for
the notification.
Dmitriy
Am 12.02.2014 16:28, schrieb Makarius:
Tests about slowness take long, but here is a presumably good point in
the published history:
Isabelle/db691cc79289
Finished Pure (0:00:10 elapsed time, 0:
Am 10.02.2014 14:18, schrieb Makarius:
On Mon, 25 Nov 2013, Dmitriy Traytel wrote:
Am 23.11.2013 19:42, schrieb Makarius:
On Mon, 28 Oct 2013, Dmitriy Traytel wrote:
> Concerning the error messages: at least you should always get >
strictly more information than without co
Zorn is supposed to move to Main together with the new (co)datatype
package. I guess it was removed from Library only by mistake.
Dmitriy
Am 26.11.2013 12:58, schrieb Lawrence Paulson:
Of course we don’t have any formal curation policy for the library, but Zorn's
lemma is a fundamental result
Am 22.11.2013 21:40, schrieb Makarius:
On Fri, 22 Nov 2013, Dmitriy Traytel wrote:
This refers to Isabelle/d71c2737ee21.
The minimal example is really minimal this time:
theory Scratch
imports Main
begin
end
In Isabelle/jEdit this loads fine. Then Control+click on Main, wait a
moment for
This refers to Isabelle/d71c2737ee21.
The minimal example is really minimal this time:
theory Scratch
imports Main
begin
end
In Isabelle/jEdit this loads fine. Then Control+click on Main, wait a
moment for the text to turn #EEE3E3, close Main.thy and Scratch.thy is
now outdated as well. The
Am 20.11.2013 15:11, schrieb Jasmin Blanchette:
Dmitriy had sent me some explanations which sessions represent the material to
be moved to HOL in either case, but I never tried it out myself. It is high
time to do that now. In particularly I would like to get a feeling for
HOL-Proofs. We al
From my angle Isabelle/f6ffe53387ef resolves [1] in a robust way. But
I'm waiting for Christian to confirm this.
Dmitriy
Am 21.11.2013 00:13, schrieb René Neumann:
If there will already be a new release, would it perhaps be possible to
merge the fix (given there is a robust one) for this 'adho
Am 05.09.2013 13:35, schrieb Florian Haftmann:
I also observed that if you use sledgehammer as old-style keyword, the
proof text is inserted after instead of just replacing
lemma
"distinct xs ⟹ n ≠ m ⟹ n < length xs ⟹ m < length xs ⟹ xs ! n ≠ xs ! m"
sledgehammer by (metis distinct_conv_n
This looks interesting and useful. I think the command should take a
method as input and apply it, i.e.
explore meth
will result in
proof meth
...
qed
However when writing this, I notice that rather than "explore", I want
to use a plain "apply" and have a button/pop-up "Isarify state" shown
Am 04.08.2013 18:57, schrieb Florian Haftmann:
For nonnested recursive datatypes, compatibility is quasi-100%; and for nested
datatypes, the package will support an optional "nested to mutual" reduction to
simulate the old package, so that the same theorems as before are available
(albeit under d
Am 25.07.2013 04:16, schrieb Christian Sternagel:
Dear developers,
While the following lemma is proved automatically
lemma converse_subset:
"A¯ ⊆ B¯ ⟷ A ⊆ B" by auto
I'm not sure exactly how, since "simp_trace" shows no application of
simplification rules and neither of the rules suggeste
This is really useful! Cf. e.g. 58b87aa4dc3b.
Sometimes there is distracting output by the "auto" tools: e.g. at
http://isabelle.in.tum.de/repos/isabelle/file/58b87aa4dc3b/src/HOL/BNF/Examples/ListF.thy#l102
a "Code generator: dropping subsumed code equation" by Auto Quickcheck
and at
http://
ithout ever using a ctxt)?
cheers
chris
On 07/11/2013 02:57 PM, Dmitriy Traytel wrote:
Hi Chris,
I think Variable.polymorphic is what you want to use before using
fastype_of.
Dmitriy
Am 11.07.2013 05:12, schrieb Christian Sternagel:
Dear list,
what is the proper way of obtaining
Hi Chris,
I think Variable.polymorphic is what you want to use before using
fastype_of.
Dmitriy
Am 11.07.2013 05:12, schrieb Christian Sternagel:
Dear list,
what is the proper way of obtaining a type from a term, in case I want
to give it as argument to Sign.typ_unify (of Sign.typ_match fo
Am 15.05.2013 16:34, schrieb Makarius:
On Wed, 15 May 2013, Dmitriy Traytel wrote:
Am 15.05.2013 15:48, schrieb Makarius:
What is still unclear to me after so many years of testboard is how
it actually used in practice. I just do "isabelle build -j4 -a -d
'$AFP'" to
Am 15.05.2013 15:48, schrieb Makarius:
What is still unclear to me after so many years of testboard is how it
actually used in practice. I just do "isabelle build -j4 -a -d
'$AFP'" to see immediately how everything works out. It is also
possible to make a quick integrity check via "isabelle b
Hi all,
since "Containers" are in the AFP mira results in global crashes of the
build tool
(http://isabelle.in.tum.de/testboard/Isabelle/report/2cef0644d3d7416f8d7cea92e24fd694).
By global I mean that no session is built at all due to an outdated (wrt
Isabelle repository, e.g. 916271d52466) i
On 24.04.2013 16:18, Brian Huffman wrote:
On Wed, Apr 24, 2013 at 2:52 AM, Dmitriy Traytel wrote:
However, your example is still not printed as expected (assuming that the
output should be equal to the input in this case):
"(case x of (a, b) => λ(c, d). e) y"
Usually "pro
uot;
:: "'e"
I assume this is a result of the recent changes to the handling of
case expressions?
- Brian
On Wed, Apr 10, 2013 at 9:16 AM, Dmitriy Traytel wrote:
* Nested case expressions are now translated in a separate check
phase rather than during parsing. The data fo
ecific attribute, might it be possible to get HOLCF case
expressions to work with the new translation check phase?
- Brian
On Wed, Apr 10, 2013 at 9:16 AM, Dmitriy Traytel wrote:
* Nested case expressions are now translated in a separate check
phase rather than during parsing. The data for case
* Nested case expressions are now translated in a separate check
phase rather than during parsing. The data for case combinators
is separated from the datatype package. The declaration attribute
"case_tr" can be used to register new case combinators:
declare [[case_translation case_combin
Hi,
theory Scratch
imports Main
begin
term "True x"
thm "TrueI[OF TrueI]"
end
behaves very strangely in jedit with Isabelle/5dbe537087aa. For both
commands there is no indication of errors (except of the absence of a
popup). This seams to apply to all Isar commands involving
Toplevel.no_tim
Hi Clemens,
On 17.03.2013 20:43, Clemens Ballarin wrote:
Dear Developers,
What it the current best practice for testing my change to Isabelle?
There used to be testboard, but I'm unsure how that evolved. Is there
a similar service for testing my change to Isabelle against the AFP?
I do use
No one knows if somebody is doing something wrong.
I did a fresh clone (from the topmost non corrupted changeset) once
again. Few commits are missing (I think by Jasmin and Sascha), as I
didn't have them locally. You are both welcome to repush through
lxbroy10 (please avoid macbroy20-29).
An
I'm looking intro it.
Dmitriy
On 21.12.2012 04:07, Christian Sternagel wrote:
Dear all,
just now, when I tried
hg in
in the development repo, I got the error below. My mercurial version
is 2.2.3 (for at least some weeks). Did anybody else experience
similar problems?
cheers
chris
com
On 17.12.2012 15:45, Makarius wrote:
On Mon, 17 Dec 2012, Dmitriy Traytel wrote:
On 17.12.2012 15:23, Makarius wrote:
On Thu, 13 Dec 2012, Dmitriy Traytel wrote:
I use Mercurial 2.2 and after pushing ed6b40d15d1c the attached
error log was generated. hg verify on the server says that
On 17.12.2012 15:23, Makarius wrote:
On Thu, 13 Dec 2012, Dmitriy Traytel wrote:
I use Mercurial 2.2 and after pushing ed6b40d15d1c the attached error
log was generated. hg verify on the server says that c4a27ab89c9b is
the first damaged changeset. The corrupted repository is still on the
).
Dmitriy
On 13.12.2012 13:58, Dmitriy Traytel wrote:
The test run was ok, but the repository is corrupted once again.
Trying to repair by stripping.
Dmitriy
On 13.12.2012 13:23, Dmitriy Traytel wrote:
It worked for me. I'm currently building (or more precisely running
the build
The test run was ok, but the repository is corrupted once again. Trying
to repair by stripping.
Dmitriy
On 13.12.2012 13:23, Dmitriy Traytel wrote:
It worked for me. I'm currently building (or more precisely running
the build tool ;-) ) and will push if it succeeds.
Dmitriy
On 13.12
It worked for me. I'm currently building (or more precisely running the
build tool ;-) ) and will push if it succeeds.
Dmitriy
On 13.12.2012 12:53, Tobias Nipkow wrote:
I tried to apply your patch but failed (see below). Since I had a problem with
somebody else's patch before, I wonder if some
Hi all,
the following produces a "Loose bound variable" with Isabelle/4a15873c4ec9
theory Scratch
imports Main
begin
lemma "finite {y |y. ∃x. y ∈ f x}"
apply simp
oops
end
Fortunately, jedit treats a proof that used to work (but fails now due
to the above) as a sorry, such that I can continu
Hi all,
On 19.08.2011 01:38, Gerwin Klein wrote:
Should we ask a wider audience (isabelle-users) if anybody else has
good reasons against/for a change?
Another small advantage of set as an own datatype arises in the context
of subtyping.
We use map functions to lift coercions between base typ
99 matches
Mail list logo