Am 07.05.2013 um 09:59 schrieb Fabian Immler <imm...@in.tum.de>: > For conceptual advances, there has also been the idea of providing a slot for > "pragmas" for serializers: > One use-case is the need to add pragmas for the target language in the > generated code, but they could also be used to advise a serializer to export > only specific constants -- and these pragmas could be generated e.g. by the > export_code statement.
Another use case for pragmas would be the option to add (or modify) the (at the moment) hard-coded import statements, as proposed in [1]. Best, Fabian [1] http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/6887 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
