It doesn't seem like subst_tac had anything to do with it. I still have no
idea about what made HOL-Proofs slower on at-poly-e beween September 13
and 14. The log reveals nothing special, except a truncation at the end.
(while processing Predicate.thy). My personal inclination would be to
Hi Andreas,
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.
interesting aspect. I will take this up after the discussion aroung the
future of interpretation.ML has been settled.
Cheers,
Ultimately there is this error:
### java.lang.NoClassDefFoundError: Generated_Code$Typerep (wrong name:
Generated_Code$typerep)
That looks like a general weakness of the code generator. I have
called the file-system
insensible in the log message, but such file-systems are
common-place
The situation involving ZF can go either way, as there are hardly any users.
How are negative integers written in ZF now? Can one still write #-3 or is it
$- #3?
The first one. Numerals in ZF are left as they are, *signed*.
Florian
--
PGP available:
a) for lists: sum_list (← listsum), prod_list (← listprod)
b) for multisets: Sum_mset (← msetsum), Prod_mset (← msetprod)
c) for finite sets: Sum (← setsum), Prod (← setprod)
I assume a) means Sum_list and Prod_list?!
Why Sum and not Sum_set in c)? Is the intention that the canonical type
