My bad, should be fixed now.
- Jo
Am Dienstag, den 18.10.2016, 20:40 +0200 schrieb Florian Haftmann:
> >
> > isabelle: fb5c74a58796 tip
> > afp: c03838321f2a tip
> > *** No such file:
> > "/mnt/home/haftmann/data/tum/isabelle/devel/src/HOL/Probability/Ess
> > ential_Supremum.thy"
> > *** The
You may want to use
hg archive ~/Fishe-Yates.tar.gz
in the future.
- Johannes
Am Dienstag, den 04.10.2016, 13:18 +0200 schrieb Manuel Eberl:
> Oh, that is quite possible. Sorry about that. I typically keep my
> prospective AFP entries in private HG repositories and then simply
> tarball
Also Brian's theories are still in HOL-Library (i.e. Inner_Product and
Product_Vector). I would also move Convex back. It was split of
Convex_Euclidean_Space to be usable in Probability. Which is not
necessary anymore as Probability is based on Analysis.
I will move these files.
- Johannes
Am
There is even a third one: ∄!
I would vote to forbid the multiple variable case. At least for the
next release. Is it possible to restrict this by a mixfix syntax or
does it require to write a ML parse translations.
- Johannes
Am Dienstag, den 13.09.2016, 10:30 +0200 schrieb Tobias Nipkow:
>
Am Montag, den 08.08.2016, 15:03 +0100 schrieb Lawrence Paulson:
> Thank you for making this change!
>
> >
> > My idea would be to rename both integrals into something like:
> > has_bc_integral, bc_integrable, bc_integral,
> > has_hk_integral, hk_integrable, hk_integral
> > and consequently
* Renamed session HOL-Multivariate_Analysis to HOL-Analysis.
* Moved measure theory from HOL-Probability to HOL-Analysis. When importing
HOL-Analysis some theorems need additional name spaces prefixes due to name
clashes.
INCOMPATIBILITY.
The incompatibility is obviously due to the renaming,
I also would vote for option 3.
But is it possible to adapt all lemmas accordingly? I could imagine
that some statements use the fact that the support of multiplicity are
the prime numbers.
- Johannes
Am Dienstag, den 19.07.2016, 12:09 +0100 schrieb Lawrence Paulson:
> This is what I would do
Am Freitag, den 15.07.2016, 11:30 +0200 schrieb Makarius:
> On 14/07/16 17:50, Lawrence Paulson wrote:
>
> >
> > What’s unfortunate is that the “negated exists” quantifier is
> > available
> > both for input and output in Isabelle, just not as a TeX macro.
> The macro is available here (nipkow
Am Freitag, den 15.07.2016, 12:15 +0200 schrieb Tobias Nipkow:
> LaTeX build problems are not infrequent and could be avoided easily
> if "build"
> produced the document by default.
>
> Tobias
+1
- Johannes
> On 14/07/2016 17:50, Lawrence Paulson wrote:
> >
> > The recent failure in
Am Sonntag, den 10.07.2016, 22:37 +0200 schrieb Lars Hupel:
> Dear AFP developers,
>
> some of you may have noticed that the "AFP devel" pages have not been
> updated since April. This is partly my fault because I migrated the
> infrastructure and partly not my fault because the scripts to
Am Dienstag, den 05.07.2016, 20:02 +0200 schrieb Florian Haftmann:
>
> >
> >
> > What about adding it to the ab_group_add typeclass? I know this is
> > not
> > the usual mathematical syntax for permutations, but at least we can
> > reuse a lot of theorems from this type class.
> There *is*
Ah sorry, my previous email should have been a response here.
Very nice!
One question: why did you only set it up for monoid_mult and inverse,
and not as a ab_group_mult?
- Johannes
Am Montag, den 04.07.2016, 21:25 +0200 schrieb Florian Haftmann:
> Hi all,
>
> see 59803048b0e8 for some
Very nice!
One question: why did you only set it up for monoid_mult and inverse,
and not as a ab_group_mult?
- Johannes
Am Montag, den 04.07.2016, 21:13 +0200 schrieb Florian Haftmann:
> Hi all,
>
> in 1a474286f315 I have introduced a locale for (total) bijections,
> allowing to obtain
Hi Mathias,
there is at least the type class 'canonically_ordered_monoid' which has
the property a <= b <--> ?c. a + c = b which implies 0 <= a for all a.
Are the multisets already in this typeclass?
- Johannes
Am Dienstag, den 28.06.2016, 10:04 +0100 schrieb Mathias Fleury:
> Dear
Yes I second that. It surely is a good idea to just use it only as a
input translation.
- Johannes
Am Samstag, den 02.07.2016, 21:08 +0200 schrieb Florian Haftmann:
> Hi all,
>
> since cf26dd7395e4, ‹surj f› is a mere abbreviation for ‹range f =
> UNIV›. This is a little bit unfortunate
Unfortunately it is not easily upgraded, as I did a semantic change in
HOL-Probability (i.e. ereal -> ennreal).
My local version of MFMC is currently 25% ported, and I hope to be
finished in a couple of days. (I didn't work on it over the long
weekend)
- Johannes
On Mo, 2016-05-30 at 23:28
I will take care of it next week.
- Johannes
On Do, 2016-05-12 at 11:58 +0100, Lawrence Paulson wrote:
> There are multiple failures in PMF_OF_List. It looks like the
> behaviour of simplification has changed concerning the functions
> ennreal and ereal.
> Larry
>
> >
> > On 12 May 2016, at
Argh, the change to the AFP broke the entire build by accidentally
removing `Ergodic_Theory/document/root.tex`. I don't know how this
happened. It is fixed now. Sorry for the inconvenience.
- Johannes
Am Donnerstag, den 14.04.2016, 15:57 +0200 schrieb Johannes Hölzl:
> In HOL-Probabil
Am Donnerstag, den 10.03.2016, 11:00 +0100 schrieb Florian Haftmann:
> Hi all,
>
>
> traditionally, syntax for lattice operations (⊓ ⊔ ⊥ ⊤ etc.) has been
> kept in a separate library theory, to allow use of that quite generic
> notation for unforeseen applications.
>
> Meanwhile
or are
> there
> more examples (e.g. in the AFP)? If yes, the code generator could be
> equipped to treat particular constants *not* as class parameters.
>
> Cheers,
> Florian
>
> Am 11.01.2016 um 12:00 schrieb Johannes Hölzl:
> >
>
Am Dienstag, den 12.01.2016, 13:48 + schrieb Lawrence Paulson:
> This AFP entry no longer works. I think that the culprit is recent
> changes affecting the metric_space type class. See attachment.
>
> Larry
Ah, sorry I overlooked this. I will fix it.
- Johannes
; > > definition [code del]: "test = (test ×⇩F test :: ('a × 'b)
> > > > filter)"
> > > >
> > > > instance proof qed
> > > > end
> > > >
> > > > instantiation unit :: test_class
> > > > begin
> > > >
Hi,
I want to introduce uniform spaces in HOL, for this I need to introduce
a type class of the form (see the attached bundle):
class uniformity =
fixes uniformity :: "('a × 'a) filter"
Note that uniformity is a filter and not a function.
which sits between topological spaces and metric
]
declare test_Abort[where 'a=unit, code]
end
Am Freitag, den 08.01.2016, 09:56 +0100 schrieb Johannes Hölzl:
> Hi,
>
> I want to introduce uniform spaces in HOL, for this I need to
> introduce
> a type class of the form (see the attached bundle):
>
> class uniformity
The central limit theorem is now in the Isabelle repository:
* Summer 2014: Jeremy Avigad, Luke Serafin, CMU, and Johannes Hölzl, TUM
Proof of the central limit theorem: includes weak convergence, characteristic
functions, and Levy's uniqueness and continuity theorem.
http
I'm currently cleaning up the Central Limit Theorem, and I want to it
entirely to HOL-Probability.
I hope to finish this in 1 week, to get it into Isabelle 2016.
- Johannes
Am Freitag, den 01.01.2016, 20:24 +0100 schrieb Makarius:
> Isabelle2016-RC0 is published, but we are still in normal
Ah, after I read Gerwin's email, I thought it was really a problem with
find_theorems. But now you reminded me that it was the setup of
dist_norm.
As far as I remember the reason is that you want to have the syntactic
type classes when you instantiate a type to have dist and norm. But
later when
Am Sonntag, den 15.11.2015, 11:43 +0100 schrieb Andreas Lochbihler:
> Vickey_Clarke_Groves looks related to the changes to "real", but I
> have not tried to fix this.
This should be fixed now in AFP e6d87060e398.
- Johannes
___
isabelle-dev mailing
raries.
>
> Larry
>
> > On 11 Nov 2015, at 17:17, Johannes Hölzl <hoe...@in.tum.de> wrote:
> >
> > Hi Larry,
> >
> > this is a huge change and after I adapted Markov_Models I see that it
> > simplifies some proofs.
> >
> > I
Hi Larry,
this is a huge change and after I adapted Markov_Models I see that it
simplifies some proofs.
If you want I can adapt all AFP entries for which I'm the maintainer, or
which are related to Probability theory:
Density_Compiler
Integration
Lower_Semicontinuous
Markov_Models
a real :: 'a => real is required! Both introduce a type class with
group/vector-space homomorphism.
I did _not_ look yet into:
JinjaThreads
Ordinary_Differential_Equations
Affine_Arithmetic
Akra_Bazzi
- Johannes
Am Mittwoch, den 11.11.2015, 18:29 +0100 schrieb Johannes Hölzl:
> O
, like the existing ones.
I now see that there is another case:
real :: float = real
This one is injective, and a properly generic function
of_float :: real ⇒ 'a::real_algebra_1”
looks easy to define.
Larry
On 29 Jul 2015, at 15:24, Johannes Hölzl hoe...@in.tum.de wrote
The syntax is nice, but I would interpret _⇩ℕ not as of_nat but as
into nat, or more specifically I would read: _⇩ℝ == real _.
- Johannes
Am Freitag, den 05.06.2015, 23:58 +0200 schrieb Florian Haftmann:
Hi again,
after I first iteration of discussion I see a list of three requirements:
Maybe we should resurrect the idea of using adhoc overloading for the
real abbreviation.
Florian, does your rework of the generic machinery for syntactic
abbreviations include moving more of the adhoc overloading into HOL?
Then we could setup real as an adhoc overloaded constant and the proof
Sorry this was my fault.
isabelle build -a does not guarantee that the current changes are
actually committed...
BTW, can the predicate_compiler setup s.t. typedefs are ignored
automatically?
- Johannes
Am Montag, den 13.04.2015, 11:28 +0200 schrieb Makarius:
In current 7ff7fdfbb9a0 there
Merged pushed with 5fd0b3c8a355.
- Johannes
Am Montag, den 30.03.2015, 06:39 + schrieb Thiemann, Rene:
Dear all,
can someone please integrate the attached patch which introduces a
locale for semirings.
I tested the patch by running all sessions of the AFP though without
Sorry was my mistake, should be fixed with d5a3dbc9da17 now.
- Johannes
Am Sonntag, den 16.11.2014, 19:48 +0100 schrieb Florian Haftmann:
isabelle: 059ba950a657 tip
afp: 0fdf8f639bb4 tip
Running JinjaThreads ...
JinjaThreads FAILED
(see also
Fixed with 1bcf0828d38c and 7a2b867fa843.
Am Montag, den 17.11.2014, 09:13 +0100 schrieb Florian Haftmann:
isabelle: 059ba950a657 tip
afp: 0fdf8f639bb4 tip
Building HOL-Multivariate_Analysis ...
Running Sturm_Tarski ...
Running Abstract_Completeness ...
Finished Sturm_Tarski (0:00:28
Am Montag, den 03.11.2014, 10:30 +0100 schrieb Makarius:
On Mon, 3 Nov 2014, Timothy Bourke wrote:
Would it also be reasonable to allow 'text' before an initial 'theory' ?
I have asked myself that yesterday, when updating some AFP entries in that
respect.
The canonical question: Is
27.10.2014, 09:42 +0100 schrieb Johannes Hölzl:
I will fix it.
- Johannes
Am Sonntag, den 26.10.2014, 17:25 + schrieb Lawrence Paulson:
FYI: the lemma is used only once, in Real.thy, and not at all in the AFP.
Still worth fixing though. Any volunteers?
Larry
Begin
In 3094b0edd6b5 I needed to change a document comment {* ..*} to a
source comment (* .. *). Looks like using the @{ML ..} antiquotation in
a document comment does not work. Latex does not allow \verb inside
commands-parameters.
Is it possible to change \verb to \texttt, with the necessary _ - \_
Am Donnerstag, den 18.09.2014, 15:47 +0200 schrieb Florian Haftmann:
Changeset #fe083c681ed8 introduces products over lists. There has been
some private discussion whether there could be a serious attempt to
establish a new consistent naming scheme for summation and products over
collections.
However this happened at the Scala level. Nitpick produced a huge number
in Suc representation, which the output panel was only possible to
display when the Java stack size was 16MB.
- Johannes
Am Donnerstag, den 03.07.2014, 14:16 +0200 schrieb Tobias Nipkow:
Funnily enough I had the same
Fixed in AFP 833ddc4860dd.
- Johannes
Am Mittwoch, den 18.06.2014, 22:32 +0200 schrieb Florian Haftmann:
The two other failures are also reproducible interactively and seem to
result from recent changes in HOL-Probability. Johannes, I guess this
is your part.
Florian
On
Hi,
a change of mine leads to a failure of the testboard,
HOL-Proofs-Extraction can not be build anymore.
For example see:
http://isabelle.in.tum.de/testboard/Isabelle/report/8ceeff1ddd5f46b49db13d3380997d28
But when I run on this very changeset the commands
isabelle build -b
, den 04.06.2014, 10:18 +0200 schrieb Johannes Hölzl:
Hi,
a change of mine leads to a failure of the testboard,
HOL-Proofs-Extraction can not be build anymore.
For example see:
http://isabelle.in.tum.de/testboard/Isabelle/report/8ceeff1ddd5f46b49db13d3380997d28
But when I run on this very
Am Sonntag, den 11.05.2014, 04:55 -0700 schrieb Andrei Popescu:
Johannes wrote:
Theorems about complex numbers are now stated only using Re and Im,
the Complex
constructor is not used anymore. It is possible to use primcorec to
defined the behaviour of a complex-valued function.
* Theorems about complex numbers are now stated only using Re and Im, the
Complex
constructor is not used anymore. It is possible to use primcorec to defined
the
behaviour of a complex-valued function.
Removed theorems about the Complex constructor from the simpset, they are
available
for Probabilistic_Noninterference is missing!
- Johannes
Am Montag, den 05.05.2014, 11:18 +0200 schrieb Dmitriy Traytel:
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
Currently I have the problem that when opening a file in
Multivariate_Analysis it can take quite some time until the theories it
depends on are loaded. In this time I/jEdit does not respond to mouse or
keyboard input.
For example:
1) I'm opening
+1
Fortunately, nowadays the list of manuals shown in jEdit is very helpful
here.
Am Mittwoch, den 26.03.2014, 22:07 +0100 schrieb Florian Haftmann:
Hi,
since ancient times there is a glitch in the naming of manuals vs. their
originating sessions, e.g. isar-ref vs. IsarRef.
Would it be
Sorry for the inconvenience introduced by my changeset.
And thanks Brian for fixing it so fast!
- Johannes
Am Dienstag, den 18.03.2014, 12:10 -0700 schrieb Brian Huffman:
Revision c7dfd924a165 should now take care of it.
- Brian
On Tue, Mar 18, 2014 at 11:47 AM, Makarius
* Removed and renamed theorems in Series:
summable_le ~ suminf_le
suminf_le ~ suminf_le_const
series_pos_le ~ setsum_le_suminf
series_pos_less ~ setsum_less_suminf
suminf_ge_zero ~ suminf_nonneg
suminf_gt_zero ~ suminf_pos
Am Dienstag, den 26.11.2013, 11:52 +0100 schrieb Jasmin Christian
Blanchette:
The AFP tests are finally back, and this revealed a series of failures
related to my refactorings last week. Looking more closely at the
falures, I found they were all in the LaTeX generation, which I hadn't
tested
Am Dienstag, den 26.11.2013, 13:12 +0100 schrieb Makarius:
[..]
I added now Zorn to HOL-Library (isa# acb41098607a), at least
Coinductive works now.
I don't understand this at all, neither the above explanation nor the
formal changeset (with its vacuous log message).
How does the
*** HOL ***
* SUP and INF generalized to conditionally_complete_lattice
* Theory Lubs moved from HOL image to HOL-Library. It is replaced by
Conditionally_Complete_Lattices. INCOMPATIBILITY.
* Introduce bdd_above and bdd_below in Conditionally_Complete_Lattices, use them
instead of explicitly
solved in afp id 03689082b646
Am Dienstag, den 05.11.2013, 19:09 +0100 schrieb Florian Haftmann:
isabelle id 9d623cada37f
afp id 68e8895167cc
___
isabelle-dev mailing list
isabelle-...@in.tum.de
Hi *,
code_abort does not remove the corresponding code equations
(in Isabelle 19764bef2730)
definition test = True
code_abort test
value [code] test -- outputs True
definition [code del]: test2 = True
code_abort test2
value [code] test2 -- raises 'test' exception
Should code_abort
Am Mittwoch, den 24.04.2013, 11:45 +0200 schrieb Tjark Weber:
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
Am Donnerstag, den 25.04.2013, 10:56 +0200 schrieb Johannes Hölzl:
I also renamed the type class linear_continuum_topology to
connected_linorder_topology as they are not compact spaces. If somebody
knows a better name for these spaces I'm also happy to rename them.
Okay, forget
This sums up the cleanup / generalizations / unifications I did on
HOL-Complex_Main and HOL-Multivariate_Analysis in the last four month.
9 --
* Introduce type class conditional_complete_lattice: Like a complete
lattice but does not assume the
Am Freitag, den 05.04.2013, 14:16 +0200 schrieb Makarius:
On Fri, 5 Apr 2013, Johannes Hölzl wrote:
It looks like the problem is somewhere in the call to
Classical.inst0_step_tac in nodup_depth_tac (clasimp.ML):
clasimp.ML
fun nodup_depth_tac ctxt m i st
Hi,
In Isabelle2013 as well as the current development revision (#0a7b4e0384d0)
the following call to auto raises a TYPE exception in envir.ML
8
theory Scratch
imports Main
begin
class test =
fixes P :: 'a set ⇒ bool
lemma
shows P_UNIV [intro]: P UNIV
and P_Int [intro]: P S
Hi Isabelle-dev,
there is a bugproblem with the let-simproc, resulting in a non
terminating simp call (Isabelle hg id = 58e2d0cd81ae, tip of
isabelle-release):
theory Scratch imports Complex_Main begin
lemma (let x = Collect P in R x x ∧ (Ball s P)) = X
using [[simp_trace]]
apply
Am Freitag, den 14.12.2012, 13:25 +0100 schrieb Makarius:
On Thu, 13 Dec 2012, Dmitriy Traytel wrote:
Stripping did not work (even on lxbroy10 with some older Mercurial).
However, Johannes managed to apparently fix everything by doing a fresh
clone, copying some files (such as hgrc) and
* Further generalized the definition of limits:
- Introduced the predicate filterlim (LIM x F. f x : G) which expresses that
when the input values x converge to F then the output f x converges to G.
- Added filters for convergence to positive (at_top) and negative infinity
(at_bot).
* HOL/Multivariate_Analysis:
Replaced basis :: 'a::euclidean_space = nat = real and
\Chi\Chi :: (nat = real) = 'a::euclidean_space on euclidean spaces by
using the inner product _ \bullet _ with vectors from the Basis set.
\Chi\Chi i. f i is replaced by SUM i : Basis. f i *r i.
With
Am Montag, den 10.12.2012, 15:27 +0100 schrieb Makarius:
On Tue, 27 Nov 2012, Johannes Hölzl wrote:
We had again a problem with the repository. We fixed it by using again
hg verify
hg strip failing rev according to verify
now it works again (at least on my machine and on the web
Am Montag, den 10.12.2012, 16:39 +0100 schrieb Jasmin Blanchette:
Am 10.12.2012 um 16:33 schrieb Makarius:
After the update these machines have very new Mercurial 2.4, so it could be
a communication problem with your local Mercurial and the version that it
runs via ssh.
How is the
Am Mittwoch, den 05.12.2012, 21:50 + schrieb Gerwin Klein:
On 05/12/2012, at 6:31 PM, Tobias Nipkow nip...@in.tum.de wrote:
Can anybody still build the AFP on some machine?
I have been able to build everything on a linux machine late last
night.
The only entry that comes up with an
Am Dienstag, den 04.12.2012, 15:13 +0100 schrieb Jasmin Blanchette:
Am 04.12.2012 um 15:06 schrieb Makarius:
If you provide a state where the SMT_Examples session can reproduce its
proofs,
I'll try to. Last time I regenerated the certificate, there were a couple of
cases where I was
Fabian and I found the missing check in Cooper's algorithm
(src/HOL/Tools/Qelim). The fix can be found in the testboard
52e97a5f5e25. If it works I will push it to the Isabelle repository.
- Johannes
Am Samstag, den 01.12.2012, 22:01 +0100 schrieb Florian Haftmann:
In rev. 544764f4324d
* HOL/Probability:
- Add simproc measurable to automatically prove measurability
- Add induction rules for sigma sets with disjoint union
(sigma_sets_induct_disjoint)
and for Borel-measurable functions (borel_measurable_induct).
- The Daniell-Kolmogorov theorem (the existence the
Am Donnerstag, den 08.11.2012, 09:40 +1100 schrieb Gerwin Klein:
[..]
The solution may be to just increase timeouts. On the other hand, this
whole thing used to work just fine and started to go haywire
2012-10-19, then the log files are cut off in the middle at
HOL-Probability (probably
HOL-Probability (in Isabelle/bb5db3d1d6dd) and
Ordinary_Differential_Equations (in AFP/e9fa38f86b76) work now with this
patch.
A surprising change is found in Markov_Models:
We get an error when an assumption has the same name as a fact in the
locale:
locale loc
begin
lemma X:
Am Sonntag, den 07.10.2012, 18:06 +0200 schrieb Lars Noschinski:
On 07.10.2012 09:37, Florian Haftmann wrote:
Hi all,
currently, theorem names in locales can be shadowed (given that
declarations are in different theories, otherwise the foundation level
would reject the declaration since
Hi Makarius,
For the mkroot tool I would suggest that the layout looks more like a
AFP submission. The resulting directory should contain everything:
$ isabelle mkroot Project_X
Results in:
Project_X/ROOT
Project_X/Project_X.thy
Project_X/document/root.tex
Also instead of calling the
Am Donnerstag, den 26.04.2012, 14:09 +0200 schrieb Makarius:
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
Am Montag, den 23.04.2012, 17:22 +0200 schrieb Makarius:
Here is an update of the test website for warming up a bit more
http://www4.in.tum.de/~wenzelm/test/website/
I've spent this cold and wet weekend to produce a monolitic Windows
application, which bundles both JDK and Cygwin 1.7.9,
Hi Isabelle users developers,
we have now a wiki for the Isabelle community:
http://isabelle.in.tum.de/community
It is intended for:
* the lists which are always outdated, like
- FAQ,
- projects people working on,
- theory collections,
- external tools,
- ...
These
Am Montag, den 14.11.2011, 19:27 +0100 schrieb Florian Haftmann:
Hi Johannes,
two remarks:
* http://isabelle.in.tum.de/reports/Isabelle/rev/e828ccc5c110
With `notepad` you can prove everything without a trace in theory, which
eliminates the need for fiddling around with quick_and_dirty.
Am Montag, den 14.11.2011, 21:05 +0100 schrieb Alexander Krauss:
On 11/14/2011 08:43 PM, Johannes Hölzl wrote:
Am Montag, den 14.11.2011, 19:27 +0100 schrieb Florian Haftmann:
Hi Johannes,
two remarks:
* http://isabelle.in.tum.de/reports/Isabelle/rev/e828ccc5c110
With `notepad
I changed the default encoding from iso8859-1 to utf-8 for the normal
website. The theory documentation is kept in iso8859-1 (e.g. latin-1),
this will change with Isabelle2011.
So, when the mirrors are updated everything should be fine again.
Greetings,
Johannes
Am Donnerstag, den
Am Mittwoch, den 01.09.2010, 15:40 +0200 schrieb Makarius:
For some week or so there are sparadic failures of HOL-Decision_Procs like
this:
[..]
This only happenes when running in parallel mode, which is the default
on modern hardware for quite some time already. I estimate the
probability
Am Montag, den 17.05.2010, 09:41 -0700 schrieb Brian Huffman:
[..]
build times slower by a similar factor? I don't think users would be
very pleased if the new version of Isabelle takes twice as long to
process their old theories.
Today I discoverd a simple procedure to speed up the build time
* Changed DERIV_intros to a NamedThmsFun. Each of the theorems in
DERIV_intros
assumes composition with an additional function and matches a variable
to the
derivative, which has to be solved by the simplifier. Hence
(auto intro!: DERIV_intros) computes the derivative of most elementary
terms.
*
86 matches
Mail list logo
