8fcbfce2a2a9 tip
- René
--
René Neumann
Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München
Tel: +49-89-289-17232
Office: MI 03.11.055
smime.p7s
Description: S/MIME Cryptographic Signature
on it in the NEWS file.
Is there something I missed?
Thanks,
René
--
René Neumann
Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München
Tel: +49-89-289-17232
Office: MI 03.11.055
smime.p7s
Description: S/MIME Cryptographic Signature
entries that are not listed in the keywords
file.
'isabelle keywords $SESSION' can be used to generate a new keywords file
with all keywords of $SESSION.
- René
--
René Neumann
Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München
Tel: +49-89-289
If there will already be a new release, would it perhaps be possible to
merge the fix (given there is a robust one) for this 'adhoc_overloading
raises TYPE' issue [1] ?
This error is quite puzzling. And it occurs even if one does not know
what the packages 'adhoc_overloading' and 'coercions' are
reluctant about using the Arith.* functions in
my handwritten SML-code (relying on generated stuff etc), hoping that
there was something automagical. But now where you've stated that it's
the way to go, I've done it like that.
- René
--
René Neumann
Institut für Informatik (I7)
Technische
:: integer = integer
where foo_wrap x = x + 1
lemma [code]:
foo x = nat_of_integer (foo_wrap (integer_of_nat x))
Or am I using the new theories in a wrong fashion / there is automation
I could use?
Thanks,
René
P.S.: Hopefully, this is the right mailinglist.
--
René Neumann
Institut für
Am 06.08.2013 16:41, schrieb René Neumann:
It is probably related to the thread Subscripts within identifiers,
but I'm not definitly sure.
Most definitly: This behavior has been introduced with rev 3ac2878764f9.
The question that remains (I could not grok it from the other thread):
Is it now
