On Fri, 2008-09-26 at 04:25 +0200, Alexander Krauss wrote:
So the only realistic chance is that users keep up with the development
and update their theories.
Two (not necessarily great, as there is a tradeoff) ideas to assist with
that:
- Isabelle version headers in theory files (e.g.,
On Fri, 2008-10-03 at 14:14 +0200, Florian Haftmann wrote:
I also think that two would be better than three; technically
undefined is the same as arbitrary
Then what is the point of
undefined_fun: undefined x = undefined
in HOL.thy?
Best,
Tjark
On Sun, 30 Nov 2008, Makarius wrote:
After several months of getting acquainted with distributed version
control in general, we should be finally ready to switch the official
Isabelle repository to Mercurial.
I noticed that Mercurial does not perform CVS keyword expansion by
default, causing
On Tue, 2008-12-02 at 22:09 +0100, Makarius wrote:
With Mercurial you have the whole history always around, and there is no
need to encode (tiny) parts of it in the file.
Certainly $Id$ keys are rather useless as long as the file is part of a
managed repository. However, files escape into the
On Tue, 2009-07-14 at 11:19 +0200, Makarius wrote:
[...] contributors are urged to document user relevant changes
as soon as possible, in order that things are not forgotten for the
release. (I reckon that half of the changes after Isabelle2009 have not
shown up in NEWS yet.)
[...]
On Fri, 2009-08-21 at 19:19 +0200, Dennis Walter wrote:
The following proof works fine if QuickDirty is enabled, i.e. in
interactive mode. But if this proof is re-run with QD turned off
(e.g. in batch mode), the proof fails, because arith yields the error
displayed below.
lemma [| 1 =
On Tue, 2009-11-17 at 15:18 +0100, Makarius wrote:
A repository clone is not a proper distribution, and various parts are
missing. The Admin/build script helps to fill these gaps, notably
Admin/build browser
Clemens used to maintain a web page with installation instructions for
the
On Wed, 2010-08-04 at 11:50 +1000, Thomas Sewell wrote:
It occurs to me that I don't even know whether theorems in Isabelle
can be assumed to be beta/eta normal. Does anyone have any quick
pointers on that? Is there a potential bug here?
There are various pieces of code that expect terms and
On Fri, 2010-09-03 at 15:06 +0200, Makarius wrote:
When composing log messages it is important do this from the perspective
of someone who needs to figure out problems many months/years later, and
needs to understand what was truely happening at some point.
tuned
Regards,
Tjark
I've recently worked on an algebraic hierarchy, ranging from semi-groups
to Kleene algebras and related structures, in Isabelle/HOL. It goes
without saying that Isabelle's local specification mechanisms were well
suited for the task. However, using classes and locales more
extensively for the
Clemens,
Thanks for your quick reply!
On Thu, 2010-12-16 at 20:37 +0100, Clemens Ballarin wrote:
Suggestions? The message also says that the relation is probably not
terminating.
Well, roundup bound is developer jargon. Sublocale relation probably
not terminating points into the right
On Thu, 2011-01-13 at 22:15 +1100, Gerwin Klein wrote:
On 13/01/2011, at 8:51 PM, Larry Paulson wrote:
Accented characters on our website no longer display correctly on
Macs. I don't know precisely when this happened, but I'm sure it's
fairly recent. In fact, the characters don't even
Hi,
I noticed that numerous lemmas in HOL that refer to class constants are
stated at the top level (using implicit or explicit sort annotations),
rather than in the corresponding class context (see, for instance,
Compl_lessThan in HOL/SetInterval.thy). If I am not mistaken, this
means the
On Fri, 2011-01-21 at 15:27 +0100, Tobias Nipkow wrote:
One issue can be that if some sort involves multiple type classes, the
corresponding class may not have been defined. That is the one advantage
of sorts: you can create conjunctions/intersection of type classes on
the fly.
If there is
On Fri, 2011-01-21 at 07:27 -0800, Brian Huffman wrote:
On Fri, Jan 21, 2011 at 7:03 AM, Tjark Weber webe...@in.tum.de wrote:
Of course, this doesn't work for lemmas that involve separate sorts.
I'm not sure if this is what you have in mind, but in HOLCF there is a
continuity predicate
On Tue, 2011-02-08 at 06:53 -0800, Brian Huffman wrote:
Honestly, I think the above parsing rules are quite confusing, and
should be changed. I instantiate variables in theorems quite often,
and many theorems use variable names that end in digits, but I almost
never need to refer to variables
Hi,
Attempting to define
fun f where f 0 = undefined
in Isabelle/HOL (7f2793d51efc) yields
*** exception TYPE raised (line 38 of
.../isabelle/src/HOL/Tools/Function/pattern_split.ML): inst_constrs_of
*** At command fun
A more user-friendly error message would be nice.
Kind regards,
Tjark
On Sat, 2011-05-21 at 15:12 -0700, Brian Huffman wrote:
I just noticed this error message from primrec [...]
What is the status of primrec anyway, in the light of fun(ction)?
Kind regards,
Tjark
___
isabelle-dev mailing list
isabelle-...@in.tum.de
On Tue, 2011-07-05 at 13:27 +0200, Gerwin Klein wrote:
500:
643.64
3421.79
I may be stating the obvious, but in my (general) experience, profiling
large examples like these (and subsequent code optimization) can often
lead to drastic performance improvements if it hasn't been done before.
On Thu, 2011-08-18 at 09:34 +0200, Jasmin Christian Blanchette wrote:
The maintenance load is extremely low. When it comes to the REFUTE
exception, I can look at it if and when we decide to move back to
sets.
I suspect that Jasmin will have no trouble fixing this, but otherwise
I'd be happy to
On Sat, 2012-01-14 at 14:34 +0100, Tobias Nipkow wrote:
- If one of them is singled out as fold, then it should be foldr,
not foldl [...]
This is correct, of course; also because foldr can be generalized to
catamorphisms on arbitrary algebraic data types. In other words, foldr
is the canonical
On Thu, 2012-04-26 at 14:09 +0200, 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
On Tue, 2012-06-26 at 22:46 +0200, Florian Haftmann wrote:
Tiny instructions on changesets c97656ff4154 ff.:
[...]
The Isabelle Wiki has a HOWTO on Working with the repository version
of Isabelle (at
https://isabelle.in.tum.de/community/Working_with_the_repository_version_of_Isabelle).
Perhaps
Hi,
Ctrl-click in Isabelle/jEdit exposes additional information - about
the next best thing since sliced bread. I have a few suggestions for
related features that would be nice to have, in my opinion (provided
they are not too much implementation work):
1) In theory T imports A, I'd like to be
Hi,
Building the repository version (7476665f3e0f) with isabelle build -a
generates a number of files that Mercurial doesn't know about (see
below). I could simply add them to .hgignore, but perhaps someone who
knows why these files are generated would be more qualified to do so?
Best regards,
On Tue, 2012-08-14 at 17:09 +0200, Makarius wrote:
Building the repository version (7476665f3e0f) with isabelle build -a
generates a number of files that Mercurial doesn't know about (see
below).
That is normal for people who are used to build the doc-src stuff
occasionally. The
Christian,
On Wed, 2012-08-08 at 14:17 +0900, Christian Sternagel wrote:
the script you introduced in
http://isabelle.in.tum.de/repos/isabelle/rev/c895e334162c
is rather useful. How about also providing a variable (as TMP for the
download directory) to set the actual isabelle tool
On Wed, 2012-08-08 at 11:22 +0200, Makarius wrote:
One could also use wget -O- ... | tar xvzf - and avoid the TMP file.
Unfortunately, this doesn't behave as one would like when wget fails.
Best regards,
Tjark
___
isabelle-dev mailing list
On Wed, 2012-08-15 at 13:22 +0200, Makarius wrote:
I will have to take a look at the component business again soon, to
simplify it further and remove features and clones of other Isabelle
scripts.
Great. I've now turned download_components into an isabelle (Admin)
tool (cf. 01d1734f779d), as
On Mon, 2012-08-27 at 13:35 +0200, Makarius wrote:
1) In theory T imports A, I'd like to be able to Ctrl-click on A to
open the corresponding theory file.
See some changesets leading up to Isabelle/10b89c127153 how I've spent
Sunday afternoon.
Nice. I suspect it would be considerably
On Fri, 2012-09-07 at 17:20 +0200, Makarius wrote:
So when the code generator sees an interpreted function application
loc.c t1 t2 t3 x y z it should somehow do the right thing, in taking it as
(loc.c t1 t2 t3) x y z, and considering the inner part as atomic
entity (and instance of c defined
On Tue, 2012-10-16 at 17:43 +0200, Tobias Nipkow wrote:
Am 16/10/2012 13:22, schrieb Tjark Weber:
Class semiring in HOL/Rings.thy [1] assumes
left_distrib: (a + b) * c = a * c + b * c
right_distrib: a * (b + c) = a * b + a * c
We should certainly not contradict the mathematical
On Sun, 2012-10-21 at 16:46 +0200, Florian Haftmann wrote:
Btw. whenever I'm testing the AFP these days without relying on the
testboard I use the following [...]
In the last few months I've seen several emails with testing advice on
this list (occasionally motivated by commits that apparently
Hi,
The new AFP entry on Kleene Algebras contains a metis call
(http://afp.hg.sourceforge.net/hgweb/afp/afp/file/082b389cb3f8/thys/Kleene_Algebra/Kleene_Algebra.thy#l652)
that generates a warning about an unused theorem local.opp_mult_def.
Not passing opp_mult_def as an argument to metis gets rid
On Fri, 2013-01-18 at 19:29 +0100, Jasmin Christian Blanchette wrote:
What's your concrete suggestion here?
It's more of a curiosity than an issue, of course. Otherwise, I would
suggest to: First, make sure that the behavior is not due to a bug or
silly inefficiency in the metis code. Second,
On Wed, 2013-01-30 at 15:14 +0100, Jasmin Christian Blanchette wrote:
First is quite a bit of work, if you want to bring it into a format
that Joe Hurd can understand, assuming he even has the time to look
into it.
It's probably not worth the effort then. Like you said, this kind of
behavior
Hi Jasmin,
On Wed, 2013-01-30 at 15:14 +0100, Jasmin Christian Blanchette wrote:
To suppress the warning, one trick is to ensure that the theorem has no
name hint, e.g.
mythm[THEN asm_rl]
or (if it's not polymorphic) pipe it in with using mythm apply -. The
first trick could be made
Hi Jasmin,
On Wed, 2013-02-13 at 09:09 +0100, Jasmin Christian Blanchette wrote:
Thankfully, there's a much easier solution:
using [[metis_verbose = false]] by (metis ...)
or, at the top-level,
declare [[metis_verbose = false]]
It's always nice to find out that a requested feature
On Fri, 2013-02-15 at 13:37 +0100, Tobias Nipkow wrote:
* Sledgehammer spontaneously acts asynchronously of certain open
problems in the text, depending on certain parameters like time outs.
Triggering s/h via sorry (or some other explicit means) is perfectly
reasonable, but having
Hi,
After hg fetch to update to tip (22ba938ab10f), followed by isabelle
components -a, Isabelle build now fails with this error message:
isabelle.XML$XML_Body
Any advice?
Tjark
___
isabelle-dev mailing list
isabelle-...@in.tum.de
On Fri, 2013-02-22 at 13:26 +0100, Makarius wrote:
I would say you just need the usual isabelle build -b -f to force a
fresh build of everything. Java stuff, and especially Scala stuff is not
100% monotone wrt. upgrades.
Thanks for the quick reply. jedit -b -f by itself didn't seem to fix
On Mon, 2013-03-18 at 12:16 +0100, Makarius wrote:
If anything is missing or wrong in README_REPOSITORY, I ask once again to
point it out, either on isabelle-dev or privately, and not to make
unreliable/unmaintained clones of such important information.
Occasionally
cd isabelle
hg pull
On Fri, 2013-03-22 at 13:25 +0100, Makarius wrote:
On Fri, 22 Mar 2013, Andreas Lochbihler wrote:
{(x, y). P} is pretty syntax for
Collect (prod_case (%x y. P)), so in your case, you get
Collect (prod_case (%v v. v : {''a'', ''b''}))
See how the second v in %v v. ... hides the former.
Johannes,
On Mon, 2013-04-22 at 16:39 +0200, Johannes Hölzl wrote:
* Introduce type class conditional_complete_lattice: Like a complete
lattice but does not assume the existence of the top and bottom elements.
The name conditional complete lattice suggests a special kind of
complete lattice.
Larry,
On Thu, 2013-05-02 at 16:18 +0100, Lawrence Paulson wrote:
I am getting a lot of poly/ML segmentation faults, and they are making
it very difficult to do my work, especially as my theories take at
least 15 minutes to load. If it then simply crashes then I'm not
getting anywhere.
Has
On Fri, 2013-07-12 at 19:41 +0200, Makarius wrote:
How would Omega Algebras fare with notation A\^sup\infinity instead
of A\^sup\omega?
Worse. Of course, a name is just that, but for clarity and convenience,
it is nice to be able to call things in Isabelle what they are called
in the
On Thu, 2013-08-01 at 16:41 +0200, Makarius wrote:
On Wed, 10 Jul 2013, Tjark Weber wrote:
Looking superficially at
http://isabelle.in.tum.de/repos/isabelle/file/b7a83845bc93/src/HOL/ex/SAT_Examples.thy
I wonder if this actually works right now.
Good question. One issue is that the theory
On Mon, 2014-01-13 at 12:38 +, Thomas Sewell wrote:
Given a hypothesis of the form x = Suc a or Suc a = x, where x is a
free (blue) variable, hypsubst will substitute Suc a for x throughout
the goal, and then discard the hypothesis. The substitution is almost
always wanted. Discarding the
On Wed, 2014-05-07 at 15:41 +0200, Makarius wrote:
How about ~~/src/HOL/ex/Sudoko.thy? It formally depends on ZCHAFF_HOME,
so it is rarely run in practice. Does it now make sense to remove that
condition in the ROOT file? What is tested in this theory anyway? The
'refute' / 'oops'
Makarius,
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.
Best,
Tjark
# HG changeset patch
# User webertj
# Date
Florian,
On Thu, 2016-03-10 at 14:01 +0100, Manuel Eberl wrote:
> "multiplicity" is definitely interesting [...]
> I don't see why is_prime should require an algebraic_semidom [...]
> Factorial rings (also known as unique factorisation domains) usually
> [...]
> [...] (somewhat non-standard)
On Tue, 2016-09-13 at 09:45 +0200, Peter Lammich wrote:
> I would have expected:
> (∄x y. P x y) ⟷ ¬(∃x y. P x y)
> and
> (∃!x y. P x y) ⟷ (∃!xy. P (fst x) (snd x))
+1
Best,
Tjark
___
isabelle-dev mailing list
isabelle-...@in.tum.de
On Thu, 2018-01-18 at 14:31 +0100, Tobias Nipkow wrote:
> > One possible criterion: which results
> > are part of a standard undergraduate athematics curriculum?
>
> It sounds like a reasonable criterion. Can you tell us what that means for
> Hausdorff_Distance, Metric_Completion and
This message has been automatically generated in response to the
creation of a trouble ticket regarding
Re: [isabelle-dev] Accented characters,
a summary of which appears below.
There is no need to reply to this message immediately. Your ticket has
been assigned an ID of
On Thu, 2011-01-13 at 11:48 +, Piete Brooks via RT wrote:
Indeed this appears to be a configuration issue with the Cambridge web
server.
See http://www.cl.cam.ac.uk/news/2011/01/web-server-changes/
I am surprised that the web server cannot be configured to add the UTF-8
default
55 matches
Mail list logo
