Hi everyone,
as can be seen on
http://www21.in.tum.de/~noschinl/jedit-screenshot.png,
(from Isabelle ecffea78d381 on Linux), scroll bars partially obscur the
content of a popup.
BTW, for theorems it would be pretty nifty, if the popup would show the
theorem, not only its name.
--
On Tue, 30 Oct 2012, Lars Noschinski wrote:
I deleted and reverted $ISABELLE_HOME/lib. Now everything seems to work
again. As a data point: While executing the first isa build, another
instance of this Isabelle instance was running.
This should already be sufficient to explain it: the build
On Fri, 16 Nov 2012, Lars Noschinski wrote:
Hi everyone,
as can be seen on
http://www21.in.tum.de/~noschinl/jedit-screenshot.png,
(from Isabelle ecffea78d381 on Linux), scroll bars partially obscur the
content of a popup.
BTW, for theorems it would be pretty nifty, if the popup would
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
replacements, jedit went all funny and
On Thu, 11 Oct 2012, Johannes Hölzl wrote:
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
Isabelle/5e01e32dadbe is the result of spending some hours with SML/NJ and
the ever growing HOL image. In the end it turned out as rather trivial
thing: Time.+ needs to be used in this qualified manner, since the adhoc
overloading of + on different ML systems works differently.
I can't say
