Hi Andreas,
I now pushed this the repository (1774d569b604), but I reuse the
existing constant nat_of_integer instead of a new one.
thanks for working this out so quickly!
Hi René,
does this solve all your reported problems?
Cheers,
Florian
--
PGP available:
Dear all,
Chris and I have recently ported our libraries IsaFoR and TermFun to the
development version which worked nicely, except for one issue, which arises
when we want to import external proofs into Isabelle.
The below theory compiles in Isabelle 2013 without problems.
The problem is that
Hi René,
Florian has reworked the setup for target language numerals. I can at least explain why
you run into the error and provide a workaround.
Code_Target_Nat implements the type nat as an abstract type (code abstype) with
constructor Code_Target_Nat.Nat, i.e., Code_Target_Nat.Nat must
Hi Andreas,
Code_Target_Nat implements the type nat as an abstract type (code abstype)
with constructor Code_Target_Nat.Nat, i.e., Code_Target_Nat.Nat must not
appear in any equation of the code generator. Unfortunately, this declaration
also sets up the term_of function for type nat to
