On Sat, 15 Nov 2014, Gerwin Klein wrote:
I agree that it would be nice to support that, esp since find_theorems
is supposed to help beginners find things.
Applying underscores will have unwanted side effects for other terms,
esp constants, though, so one would have to be careful to apply this
Hi Makarius,
>> I would expect that if Jasmin's plugin manager is also used in the code
>> generator, it would be easy to implement plugin selection for code_datatype,
>> too.
>
> This should work out easily with the unified Plugin_Name and Plugin concept
> of
> http://isabelle.in.tum.de/repo
On 21.11.2014 15:00, Christian Sternagel wrote:
Hi Dmitriy,
thanks for another round of clarification (I should really reread old
emails before referring to them).
On 11/21/2014 02:43 PM, Dmitriy Traytel wrote:
In general, why not create map-functions that allow to map over *all*
type parame
Hi Dmitriy,
thanks for another round of clarification (I should really reread old
emails before referring to them).
On 11/21/2014 02:43 PM, Dmitriy Traytel wrote:
In general, why not create map-functions that allow to map over *all*
type parameters. (As I understand it, this was done just a f
Hi Christian,
On 21.11.2014 14:09, Christian Sternagel wrote:
Dear list,
sorry for the subject ;)
René and I are currently at adapting the Show(_Generator) entry of the
AFP to the new datatype package. And again we stumbled across some
difficulties we already encountered when adapting the Or
Dear list,
sorry for the subject ;)
René and I are currently at adapting the Show(_Generator) entry of the
AFP to the new datatype package. And again we stumbled across some
difficulties we already encountered when adapting the Order_Generator
(and which are not resolved yet).
I think it be
