On 09/11/2013 12:52 PM, Makarius wrote:
On Tue, 10 Sep 2013, Makarius wrote:
In the meantime I have tried a few keyboards that still have a numpad
-- they usually work with page or arrow movement, but not digits.
It needs further investigation to understand which of the fixes of
jEdit key
On 16/09/2013 11:28, Makarius wrote:
On Fri, 13 Sep 2013, Makarius wrote:
I've made my own tests with the following setup:
Poly/ML SVN 1848
IsaFoR a44e26d6605e
Isabelle a49ce8d72a44
AFP 4e87a0fc2528
ML_PLATFORM=x86-darwin
On Mon, 16 Sep 2013, René Thiemann wrote:
Since the problem seems to be not that easy to fix, and since the 64-bit
mode does not seem to have this problem, would it be sensible to make
the 64-bit version the default for Isabelle on MacOS? Or are there other
known problems with the 64-bit
On Fri, 13 Sep 2013, Alexander Krauss wrote:
This refers to Isabelle f557a4645f61:
* New command fun_cases derives ad-hoc elimination rules for
function equations as simplified instances of f.elims, analogous to
inductive_cases. See HOL/ex/Fundefs.thy for some examples.
Thanks. I see that
Hallo,
The main thing still missing in Isabelle/5ccee1cb245a is a regular ML
interface Fun_Cases.fun_cases.
What do you mean by that? There exists an ML function
Fun_Cases.mk_fun_cases : Proof.context - term - thm -- is that not an
ML interface to the Fun_Cases tool? Or do you also want a
On Tue, 17 Sep 2013, Manuel Eberl wrote:
The main thing still missing in Isabelle/5ccee1cb245a is a regular ML
interface Fun_Cases.fun_cases.
What do you mean by that? There exists an ML function
Fun_Cases.mk_fun_cases : Proof.context - term - thm -- is that not an
ML interface to the
Dear all,
I have moved to jEdit about one month ago. One bug that pops up now and then is
that some letters are not displayed (on Mac OS 10.8). This has happened
irregularly over the entire month. The screenshot below as taken against
d4a4b32038eb:
On Tue, Jul 30, 2013 at 3:42 PM, Lawrence Paulson l...@cam.ac.uk wrote:
This could be a valuable service, especially for long lists of applys.
Thank you for the encouragement! I'm glad to see you agree.
(A proof like by (induct n) auto should be left alone.)
Understood. If I come across
On Wed, Jul 31, 2013 at 9:55 AM, Makarius makar...@sketis.net wrote:
On Tue, 30 Jul 2013, Josh Tilles wrote:
QUESTION STATED BRIEFLY:
If I convert existing proofs in src/HOL/**.thy from apply-style to
Isar-style, would those changes be welcome in the main repository?
It depends which
