Re: [isabelle] Separation of Isabelle/Pure and Isabelle/HOL and typedef [concerning: Isabelle Foundation & Certification]

Hi OndÅej,


> * From a technical/implementation point of view: the only conceptual
> change of the code is that you have to separate name spaces of types and
> constants in defs.ML. But because the implementation of defs.ML is
> already visionary, this is the only change that has to be done. You can
> treat type instances of type constructors and constants in an uniform
> way, i.e., there is not any change in the algorithm's itself. You just
> need a more complicated type for names of the nodes in the graph.

thanks for explaining this so thoroughly.

So, the technical complication in the first instance is a name space issue.

To maintain the Âvisionary property of defs.ML, it could also be
generalized to administrate dependencies of Ânamed symbols in general,
e.g. by using some kind of name space tagging etc. instead of hard-coded
constructors.  These could serve potential specification object logics
dealing with different kinds of entities than type constructors and
constants also, but this is highly speculative.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.