Fixed. I installed the right scala version in the right place.
Tobias
Am 15/06/2012 20:57, schrieb Florian Haftmann:
*** Code check failed for Scala: env JAVA_OPTS='-Xms128m -Xmx512m
-Xss2m' $SCALA_HOME/bin/scalac ROOT.scala *** At command export_code
(line 662 of
### Building
/2012 15:23, schrieb Makarius:
On Thu, 19 Apr 2012, Tobias Nipkow wrote:
Currently, the sort of a type variable in a type is constrained by attaching
::S to it. Right in the middel of the type, eg 'a::ord = 'a = bool.
This
can make types less readable. In Haskell this is expressed
Am 29/07/2012 03:16, schrieb Gerwin Klein:
On 29/07/2012, at 5:06 AM, Makarius makar...@sketis.net wrote:
For AFP, I would like to see a scheme without hardwired document option
within the ROOTs. Instead it can be provided for particular invocations of
isabelle build -o document=pdf etc.
Am 06/08/2012 04:33, schrieb Christian Sternagel:
Dear all,
I was wondering about the reasons for implementing list comprehension as is:
Why is an optimized translation desirable at all? Isn't that just a matter of
installing appropriate simplification rules afterwards.
Why is it
I hope you don't want to abolish isabelle make yet, because there will be many
directories out there that require it.
This reminds me: how to turn
Printer.show_question_marks_default := false;
into Isar?
Thanks
Tobias
Am 06/08/2012 12:09, schrieb Makarius:
Did everybody try the isabelle build
produces
class 'mpatch.mpatchError'Python 2.7.3: /usr/bin/python2.7
Thu Aug 16 17:59:20 2012
A problem occurred in a Python script. Here is the sequence of function calls
leading up to the error, in the order they occurred.
...
Both with firefox and safari.
Tobias
Thanks for fixing it. Unfortunately I cannot push to it anymore, it asks me for
a password.
Tobias
Am 16/08/2012 22:40, schrieb Alexander Krauss:
Quoting Makarius makar...@sketis.net:
The end of Python vomiting has this:
class 'mpatch.mpatchError': patch cannot be decoded
args =
Am 17/08/2012 15:15, schrieb Makarius:
I count this as trolling on this mailing list.
We all have our pet peeves.
Tobias
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Am 17/08/2012 21:51, schrieb Christian Urban:
On Friday, August 17, 2012 at 21:18:35 (+0200), Makarius wrote:
Tjark, you have no business here.
I assume something got here lost in translation.
Otherwise, we should all make reasonable effort
to welcome everybody on both, the
Dear Alex,
You will have seen a number of further messages on this issue. It was consensus
that the quoted sentence was not acceptable and Makarius offered his apology. I
assume that is the reaction you had hoped for and that you will continue to be
part of the community.
It seems to me that
I just rebuilt HOL. As a result I modified 3 files
M doc-src/Codegen/Thy/document/Introduction.tex
M doc-src/Codegen/Thy/document/Refinement.tex
M doc-src/Codegen/Thy/examples/example.ML
I suspect these are generated files and that the changes are the result of this
changeset: 441a4eed7823
But
Am 21/08/2012 19:48, schrieb Lawrence Paulson:
Or would it make sense to integrate this functionality with the much better
known arith method? It could then be a catchall for whatever else gets
implemented in the general realm of arithmetic. And this reminds me that we
have a great variety
Am 27/08/2012 13:35, schrieb Makarius:
It is generally a good move to develop a habit to allocate some small amounts
in
project proposals etc. for Poly/ML software maintenance and direct it to
David. This is how things can continue, and David gets a tiny little bit of
recompense for his
Am 29/08/2012 14:21, schrieb Makarius:
On Wed, 29 Aug 2012, Gerwin Klein wrote:
A small annoyance with document_output was that the output doesn't seem to
get
produced for document=false (i.e. seems to force a latex run) and that it
insists on creating a document subdirectory in the target
Am 30/08/2012 22:37, schrieb Makarius:
On Thu, 30 Aug 2012, Tobias Nipkow wrote:
I am still having some problems with it. Given
session HOL-IMP1 in ~~/src/HOL/IMP = HOL +
options [document_output=IMP-generated, document=pdf]
theories
BExp
then isabelle build -d . HOL-IMP1 puts IMP
Am 05/09/2012 15:46, schrieb Makarius:
On Wed, 5 Sep 2012, Lars Noschinski wrote:
As far as I can see, the only way to issue a successful show after a wrong
assumption (or, if you prefer, an assumption which does not fit any of the
pending goals) is discarding everything with next. So, I
Am 07/09/2012 16:51, schrieb Makarius:
On Thu, 6 Sep 2012, Tobias Nipkow wrote:
Am 05/09/2012 15:46, schrieb Makarius:
On Wed, 5 Sep 2012, Lars Noschinski wrote:
As far as I can see, the only way to issue a successful show after a
wrong
assumption (or, if you prefer, an assumption which
Am 05/09/2012 14:45, schrieb Lars Noschinski:
I like this goal; but, as you said, this is a long term process and a solution
to this particular issue does not need more then a `peepwhole view`. We also
don't deviate much from existing practice, as show does a similar trick
already.
Let me
When using jedit (development version) I got into the following situation:
partial proof
(* long
comment
*)
Because of the length of the comment (which was a lemma I had to comment out
because due to the partial proof above, proof methods in it diverged) the end of
the comment was outside
For example 03bc7afe8814
Tobias
Am 02/10/2012 20:11, schrieb Makarius:
On Tue, 2 Oct 2012, Tobias Nipkow wrote:
This is what you should not do: search and replace a string selectively that
occurs many times in a theory. I did this twice (the second time to see if it
was repeatable), using
I believe you need to do
isabelle components -a
and it will download all missing components. It's a really neat system.
Tobias
Am 04/10/2012 15:47, schrieb Lawrence Paulson:
Does anybody understand the attached message, which seems to involve the new
build system?
Larry
Am 16/10/2012 13:22, schrieb Tjark Weber:
Hi,
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
This is different from the terminology used in Wikipedia [2],
MathWorld [3] and much of the literature,
In jedit, numerals of polymorphic type are no longer tagged with the type
variable as a warning. That is an extremely helpful warning not just for
beginners, it would be a pity to lose that in jedit.
Tobias
___
isabelle-dev mailing list
Am 22/10/2012 14:16, schrieb Tjark Weber:
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
Am 27/10/2012 16:55, schrieb Makarius:
On Wed, 24 Oct 2012, Steffen Juilf Smolka wrote:
is there an implementation of priority queues in the isabelle library?
This is off-topic for this mailing list, which is for things happening around
the Isabelle development process. Unless you refer
Am 27/10/2012 18:23, schrieb Makarius:
On Sat, 27 Oct 2012, Tobias Nipkow wrote:
Am 27/10/2012 16:55, schrieb Makarius:
On Wed, 24 Oct 2012, Steffen Juilf Smolka wrote:
is there an implementation of priority queues in the isabelle library?
This is off-topic for this mailing list, which
This is exactly why I am against SMT certificates in AFP entries. Ondrej, can
you possibly remove them?
Tobias
Am 08/11/2012 11:55, schrieb Jasmin Christian Blanchette:
Hi Gerwin,
Am 07.11.2012 um 22:41 schrieb Gerwin Klein:
*** Bad certificate cache: missing certificate
*** At command
Am 16/11/2012 14:47, schrieb Makarius:
On Tue, 2 Oct 2012, Tobias Nipkow wrote:
This is what you should not do: search and replace a string selectively that
occurs many times in a theory. I did this twice (the second time to see if it
was repeatable), using Replace Find, and after about 50
For whom efficient code is a concern:
* Library/IArray.thy: immutable arrays with code generation.
Tobias
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
I believe Gerwin already reported this in some email, and I can confirm it: the
afp test hangs even on my own laptop. The trace:
lapbroy100:AFP nipkow$ isabelle afp_build -A
Building Jinja ...
Finished Jinja (0:05:06 elapsed time, 0:15:28 cpu time, factor 3.03)
Building LatticeProperties ...
, schrieb Lars Noschinski:
On 05.12.2012 08:31, Tobias Nipkow wrote:
I believe Gerwin already reported this in some email, and I can confirm it:
the
afp test hangs even on my own laptop. The trace:
lapbroy100:AFP nipkow$ isabelle afp_build -A
Building Jinja ...
Finished Jinja (0:05:06
Am 05/12/2012 16:46, schrieb Jasmin Christian Blanchette:
Am 05.12.2012 um 16:33 schrieb Tobias Nipkow:
I tried again (but after some hg fetches, and am now on 3ae4376cb739), and
now
HOL still builds but HOLCF hangs. On the other hand Johannes (running Linux
rather than MacOS) is fine
I'll look at it, thanks.
Tobias
Am 09/12/2012 12:50, schrieb Christian Sternagel:
I fixed an error that only came up during document preparation (which I should
have tested previously, sorry).
cheers
chris
On 12/09/2012 02:27 PM, Christian Sternagel wrote:
Dear all,
I have the
Am 10/12/2012 13:38, schrieb Makarius:
On Fri, 30 Nov 2012, Lukas Bulwahn wrote:
It must be considered unmaintained. The benchmarks themself I will
irregularly
have time on weekends and nights to have a look, but I cannot keep up with
Isabelle roaring ahead.
After several weeks of
Am 17/12/2012 11:34, schrieb Makarius:
On Sat, 15 Dec 2012, Florian Haftmann wrote:
Hi all,
The reason is that Open_Induction/ROOT (and also
Open_Induction/Open_Induction.thy) relies on $AFP being set, which is
only the case if AFP is registered as a component (which is not the case
for
I have just added a new theory Library/Finite_Lattice. It clashes with theory
Library/Countable in a way I don't understand. If you import both
theory Scratch
imports ~~/src/HOL/Library/Finite_Lattice ~~/src/HOL/Library/Countable
begin
Isabelle complains
Unproven class relation
In principle a good idea, but I don't think we want multiple intros for
different audiences. Hence I would aim for a general intro that also covers
points that PG users are used to.
Tobias
Am 22/01/2013 13:30, schrieb Lawrence Paulson:
Do we provide an introduction to Isabelle/jEdit for PG
Am 15/02/2013 13:12, schrieb Makarius:
On Do, 2013-02-14 at 17:22 +, Lawrence Paulson wrote:
In a dream scenario, one might imagine opening a document containing a number
of occurrences of sorry, and each one of these occurrences would be given
to
counterexample finders and to
Am 15/02/2013 14:21, schrieb Jasmin Christian Blanchette:
Am 15.02.2013 um 13:37 schrieb Tobias Nipkow nip...@in.tum.de:
Triggering s/h via sorry (or some other explicit means) is perfectly
reasonable, but having the IDE invoke s/h based on time outs and guesses
should
be avoided
Am 17/02/2013 19:41, schrieb Christian Urban:
On Sunday, February 17, 2013 at 17:06:46 (+0100), Tjark Weber wrote:
On Fri, 2013-02-15 at 13:37 +0100, Tobias Nipkow wrote:
* Sledgehammer spontaneously acts asynchronously of certain open
problems in the text, depending
Am 18/02/2013 15:10, schrieb Lawrence Paulson:
These definitions originate in Isabelle/ZF, where it is quite essential to
have a condition such as r = A * A, because otherwise no reflexive r
could exist. They aren't is obviously necessary in Isabelle/HOL, but
nevertheless the idea that the
Am 19/02/2013 03:50, schrieb Christian Sternagel:
On 02/18/2013 11:31 PM, Tobias Nipkow wrote:
Am 18/02/2013 15:10, schrieb Lawrence Paulson:
These definitions originate in Isabelle/ZF, where it is quite essential to
have a condition such as r = A * A, because otherwise no reflexive r
could
It would be better to update it. The German version is also a bit odd...
Tobias
Am 19/02/2013 00:42, schrieb Lawrence Paulson:
Leaves something to be desired. Starting with the first sentence. Do we care?
Larry
http://en.wikipedia.org/wiki/Isabelle_(proof_assistant)
Load attached theory in HOL/IMP. Go to line
done (* exception *)
and you'll see the subject line.
I am on parent: 51188:9b5bf1a9a710 tip
Tobias
Abs_Int2_ivl2.thy
Description: application/extension-thy
___
isabelle-dev mailing list
It is a fairly huge goal state that is supposed to get printed there. With all
the annotations, it may exceed the limit. But why is code generation involved at
that point (done)?
Tobias
Am 21/02/2013 15:56, schrieb Makarius:
On Thu, 21 Feb 2013, Tobias Nipkow wrote:
Load attached theory
Now that I know that this is a resource limitation and not an error, I'm happy
again.
Thanks
Tobias
Am 21/02/2013 16:51, schrieb Makarius:
On Thu, 21 Feb 2013, Tobias Nipkow wrote:
It is a fairly huge goal state that is supposed to get printed there. With
all
the annotations, it may
Am 26/02/2013 17:17, schrieb Lawrence Paulson:
A student has forwarded this problem to me. It seems weird and unbelievable.
What have I overlooked?
I tidied it up slightly (see below) but I get the same error message.
lemma True
proof -
have True = (∃x. (λy. True) x) by simp
be to blame.
Yes, your lambda y is actually a distraction.
Tobias
Larry
On 26 Feb 2013, at 16:27, Tobias Nipkow nip...@in.tum.de wrote:
The two y's are given separate types. In fact, Isabelle introduces ??'a
itself
in the process.
___
isabelle-dev
Am 27/02/2013 15:28, schrieb Makarius:
On Wed, 27 Feb 2013, Lawrence Paulson wrote:
A behaviour where ... denotes something other than the previous right-hand
side needs to be fixed.
Again this odd bug -- fixed terminology. Such problems are much deeper.
Fortunately, the solution for
Am 27/02/2013 16:44, schrieb Makarius:
On Wed, 27 Feb 2013, Tobias Nipkow wrote:
definition my0 :: nat where my0 = length []
into a definition of a constant of type 'a itself ⇒ nat with an additional
parameter. Although this is a legal definition, I never understood why this
is
done
Am 16/03/2013 01:29, schrieb Lawrence Paulson:
At d5c95b55f849
~/isabelle/Repos/src/HOL: isabelle components -a
### Missing Isabelle component:
/Users/lp15/.isabelle/contrib/jedit_build-20130104
Getting http://isabelle.in.tum.de/components/jedit_build-20130104.tar.gz;
Unpacking
Am 29/03/2013 11:24, schrieb Makarius:
On Thu, 28 Mar 2013, Manuel Eberl wrote:
I just noticed that when exporting code to Haskell, there is a complication
when some of the theories involved have lower-case names. The code export
itself will work with no error or warning, but when ghc/ghci
Holger Gast has ben added to the Unix group isabelle, if that is what you mean.
He is a member of my chair for half a year, that is why, similar to all other
members of the chair.
Tobias
Am 12/04/2013 13:08, schrieb Makarius:
This needs to be a broadcast, because there is no additional
Am 12/04/2013 13:59, schrieb Makarius:
On Fri, 12 Apr 2013, Tobias Nipkow wrote:
Holger Gast has ben added to the Unix group isabelle, if that is what you
mean. He is a member of my chair for half a year, that is why, similar to all
other members of the chair.
OK, so it is not relevant
Let me just make some remarks as a user. At ITP 2011 I published a paper
http://www21.in.tum.de/~nipkow/pubs/itp11.html where I showed how to use locales
to structure stepwise development of modules (see p11). In that context I
intentionally used the notation
interpretation (in A) B-expr
instead
I was under the impression that type synonyms are expanded in typ
antiquotations, but apparently not, at least not with 30624dab6054. If I write
@{typ vname} I get vname, even if vname is a type synonym for string. Maybe it
has always been like this, but it means that one cannot automatically
Am 27/05/2013 18:13, schrieb Makarius:
On Mon, 27 May 2013, Stefan Berghofer wrote:
As I pointed out in my previous mail, it is an error to supply disagreement
pairs to unify containing Vars that have the same name but different types.
So
I don't think one should change pattern.ML and
Am 28/05/2013 13:34, schrieb Lawrence Paulson:
Historical note: when the original high-order unification code was written,
there was no user-level polymorphism. If my memory is correct, the TVar
constructor did not even exist. Polymorphism was only used for type inference
in terms.
Am 28/05/2013 20:52, schrieb Makarius:
On Tue, 28 May 2013, Lawrence Paulson wrote:
the disagreement pairs should be fully eta-expanded by this point
I've spent further thoughts on that: somehow it increases my uneasyness, since
it looks like the full type information needs to be known at
Am 28/05/2013 23:53, schrieb Makarius:
On Tue, 28 May 2013, Tobias Nipkow wrote:
Am 28/05/2013 13:34, schrieb Lawrence Paulson:
Historical note: when the original high-order unification code was written,
there was no user-level polymorphism. If my memory is correct, the TVar
constructor did
this incident has again reminded me that in the absence of formal proofs about
the code, assertions in the code would be a big step forward. they could have
told us a long time ago that some precondition expected by the unification code
is not guaranteed. lukas and a student had even put together
Nipkow nip...@in.tum.de wrote:
Am 30/05/2013 13:49, schrieb Tobias Nipkow:
Am 30/05/2013 13:41, schrieb Lawrence Paulson:
The only question is whether Isabelle is important enough for such work to
be seen as significant in a wider context.
Makarius is right, the interaction of schematic
Am 05/07/2013 14:08, schrieb Makarius:
On Tue, 2 Jul 2013, Gerwin Klein wrote:
I'm less sure about the distinction between sub and sup. I can see it mostly
aligns with current usage patterns, but I find this distinction even more
confusing.
There are two aspects here: (1) common
Am 10/07/2013 16:54, schrieb Makarius:
That is an instance of \^supLETTER, i.e. the remaining overlap from the
earlier discussion on this thread. I have presently escaped the situation by
using \^bsup \^esup which looks almost the same in Latex, but is a bit
awkward in Isabelle/jEdit.
Why
Am 18/07/2013 22:44, schrieb Makarius:
On Thu, 18 Jul 2013, Florian Haftmann wrote:
Code generator: dropping subsumed code equation by Auto Quickcheck
I guess it would be the task the tools to omit such outbursts and not
globally on the IDE side?
In principle Context_Position.is_visible
I suspect that the csdp server may be unreachable at times.
Tobias
Am 08/08/2013 14:37, schrieb Makarius:
On Thu, 8 Aug 2013, Gerwin Klein wrote:
Tobias and I just tried from a laptop on version 41ebc19276ea, which seems to
work fine. Has somebody fixed it in the meantime?
I did not do
Am 17/08/2013 15:20, schrieb Makarius:
On Thu, 15 Aug 2013, Lawrence Paulson wrote:
I think that the only way to achieve the documented behaviour is to replace
all schematic variables in the goal by Frees before attempting resolution.
Which can be done safely outside the kernel.
If you
that these tactics
merely discard unifiers that would update the goal state. can lead to
incompleteness.
Tobias
Larry
On 19 Aug 2013, at 07:11, Tobias Nipkow nip...@in.tum.de wrote:
Am 17/08/2013 15:20, schrieb Makarius:
On Thu, 15 Aug 2013, Lawrence Paulson wrote:
I think that the only way
When you clicked on the proof generated by sledgehammer in jedit, it would
replace the sledgehammer call in the theory text with the proof, which was
*very* convenient. Alas, that has gone away recently (eg 9228c575d67d). I don't
know if it was intentional or not, the NEWS file does not seem to
Please disregard my previous email. I see that there is now a sledeghammer panel
(with some more goodies) which avoids having to type sle... and thus solves the
issue.
Thanks for that
Tobias
___
isabelle-dev mailing list
isabelle-...@in.tum.de
Am 02/09/2013 11:18, schrieb Makarius:
The sledgehammer panel has had only 1-2 rounds of refinements so far, and more
precise observations by testers on this mailing list will be required to make
it
work smoothly for the coming release.
Some observations:
- When clicking on the generated
lengthy text strings.
Larry
On 2 Sep 2013, at 11:31, Tobias Nipkow nip...@in.tum.de wrote:
- Sometimes I click on the generated proof and it is not pasted into the
theory
text. It just doesn't work, even if I click repeatedly. I cannot reproduce
this
reliably.
- Once one has clicked
For uniformity I almost always use = and would not like to see it printed as
--.
Tobias
Am 02/09/2013 16:24, schrieb Makarius:
(This is just a side-track on HOL notation, which came to me when cleaning up
theories with old ASCII replacement syntax like | -- - Un Int etc. --
which
is very
The earlier the better because, as I told you at ITP, I have a course starting
in the middle of October and they need to use a new Isabelle, in the worst case
a release candidate.
Tobias
Am 02/09/2013 15:37, schrieb Makarius:
The French summer vacation period has ended, so I've switched myself
You mean parentheses, not braces. This is an intentional change. See the NEWS:
* Weaker precendence of syntax for big intersection and union on sets,
in accordance with corresponding lattice operations. INCOMPATIBILITY.
Tobias
Am 11/09/2013 11:31, schrieb C. Diekmann:
Hi,
I just
It worked for me this morning.
Tobias
Am 17/09/2013 12:28, schrieb Lars Hupel:
I was trying to update to the repository version today, but:
$ bin/isabelle components -a
### Missing Isabelle component: /home/lars/.isabelle/contrib/jdk-7u40
Getting
I just noticed the following behaviour in 705f0b728b1b: When the cursor remains
fixed in the theory window and I scroll in that window with the help of the
scoll bar, the output window goes blank when the line with the cursor is no
longer visible. I have no idea when that changed but in Isabelle
Am 18/09/2013 17:38, schrieb Makarius:
On Wed, 18 Sep 2013, Tobias Nipkow wrote:
When the cursor remains fixed in the theory window and I scroll in that
window
with the help of the scoll bar, the output window goes blank when the line
with the cursor is no longer visible.
I have seen
Am 21/09/2013 03:08, schrieb Alessandro Coglio:
Hello,
The attached file contains a fairly heterogeneous collection of potential
extensions to the Isabelle library, which I've been developing as part of some
projects that I'm working on. I think that other Isabelle users may find them
Am 21/09/2013 03:08, schrieb Alessandro Coglio:
I also have a general question about library vs. AFP. There seem to be clear
cases of things that should go into the library (e.g. new theorems on lists or
sets) and clear cases of things that should go into the AFP (e.g. a theory of
Am 30/09/2013 12:45, schrieb Makarius:
In preparation of Isabelle2013-1 the Isabelle website needs the usual updating
and polishing.
The relevant repository is here:
https://bitbucket.org/isabelle_project/isabelle-website/
Traditionally my main job is to get the Download / Installation
Thank you for this, Florian. The one thing I had hoped for when I initiated
this change was that one can write n-1 just like n+1, but that doesn't
quite work yet, probably because you have some special syntax for what used to
be negative numerals. This may ease the conversion, but can we get rid
Am 20/11/2013 22:49, schrieb Makarius:
Are there any other potential problems of Isabelle2013-1 that were not
reported
yet?
There is a problem with autoquickcheck in Isabelle/jedit. It sometimes fails to
find or dislay a counterexample. I have a theory with a wrong lemma in it. When
I load
is loaded by proving the theory, quickcheck times out.
After the edit, there is less load, and quickcheck is faster.
--
Peter
On Do, 2013-11-21 at 10:40 +0100, Tobias Nipkow wrote:
Am 20/11/2013 22:49, schrieb Makarius:
Are there any other potential problems of Isabelle2013-1 that were
It says Timeout. Presumably this supports your guess.
Tobias
Am 21/11/2013 15:34, schrieb Makarius:
On Thu, 21 Nov 2013, Tobias Nipkow wrote:
Some such effects may indeed play a role, although I originally did not
observe
it when reloading a theory but while editing an existing theory
I just saw the above message for the first time, when building HOL-IMP. Should
this worry me?
Tobias
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Am 16/12/2013 17:21, schrieb Makarius:
On Mon, 16 Dec 2013, René Neumann wrote:
That is, have Isabelle--x and Isabelle/Tools--x.z with the
invariant that for every z Isabelle--x and Isabelle/Tools--x.z
work well together.
Again: This is just a quick idea, and I have no
On 29/01/2014 15:15, Lawrence Paulson wrote:
I’m puzzled about the inconsistency between the treatment of the new and old
number theory libraries in the file ROOT.
The old one is as I would expect, with a description and the loading of some
antecedent theories with document output
You send an email to supp...@neos-server.org. But this time I just waited and it
came back.
Tobias
On 05/03/2014 15:59, Makarius wrote:
On Fri, 21 Feb 2014, Florian Haftmann wrote:
Referring to isabelle hg id eb07b0acbebc:
HOL-Library FAILED
(see also
I set up field_simps to yield a decision procedure for field equality, provided
all denominators can be proved to be 0. Hence I am sceptical if adding new rules
to it is a good idea. Florian, can you give an example where previously
field_simps was too weak but with the two additional rules it
Florian, I was confused and you may well be right: if those two rules are no
longer simp rules, it looks like field_simps no longer does its job properly.
Most likely they should be added there as you suggested.
Tobias
On 04/04/2014 16:08, Florian Haftmann wrote:
lemma divide_minus_left
On 04/04/2014 17:37, Lawrence Paulson wrote:
A very good idea, which reduces the impact of the change on existing proofs.
I am trying it out now.
Seeing no objections, I am quite likely to push this change later today.
I don't think it is a good policy to ask for comments on a change and
?
Cheers,
Thomas.
On 05/04/14 03:09, Tobias Nipkow wrote:
I set up field_simps to yield a decision procedure for field equality,
provided
all denominators can be proved to be 0. Hence I am sceptical if adding new
rules
to it is a good idea. Florian, can you give an example where
I consider this twofold renaming of directories pointless, and as you know, it
required a twofold update in some other theories of mine. I guess I should
have stated my displeasure earlier but thought that since Makarius had already
stated he didn't even see the problem, this would discourage you.
Swap is a very generic name. There is already the qualified Fun.swap, but so
far we did not seem to need one on pairs. Hence I would not introduce an
unqualified swap on pairs now. If you find Product_Type.swap too heavy (but
how often is it used?) you could call is swap_pair. But don't just call
That works fine, thank you.
Tobias
On 11/04/2014 23:52, Makarius wrote:
On Fri, 11 Apr 2014, Tobias Nipkow wrote:
What I sometimes need is to have the latex files generated but not processed.
Currently I achieve this with a dummy root.tex file that includes nothing. Is
there a less dummy
Most useful! For fun I tried it on a text that has been read by many people and
it found another typo :-)
Thanks a lot for this
Tobias
On 14/04/2014 11:31, Makarius wrote:
*** Prover IDE -- Isabelle/Scala/jEdit ***
* Spell-checker support for document text, comments etc.
This refers to
I added a few lemmas to List and now the HOL-Proofs session no longer
terminates. This is what I got to see when I interrupted one run:
^Cpoly(52110,0xb0185000) malloc: *** mach_vm_map(size=8388608) failed (error
code=3)
*** error: can't allocate region
*** set a breakpoint in malloc_error_break
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 06:08 PM, Tobias Nipkow wrote:
I added a few lemmas to List and now the HOL-Proofs session no longer
On 14/05/2014 16:06, Makarius wrote:
On Wed, 14 May 2014, David Matthews wrote:
I don't know why it should be different when you run it interactively.
That is just because an interactive PIDE session is quite different from a
batch
build session it what it does. I've tries for years to
101 - 200 of 330 matches
Mail list logo
