Hi Frédéric, > For a few number of constants it should be possible to write all > constants by hand. For a large number, I will see how feasible it is to > generate this list of constants, or find otherwise a simpler solution...
code_reflect is definitely not intended as a watering bin. The typical
use case is import one algorithm from HOL into the ML context, with a
well-defined and minimal interface (typically, input and output types
plus one or two actual calculations).
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
