[isabelle] command "types" on Isabelle 2012



Hi all,

I am starting with Isabelle/Hol and I have some doubts (millions in fact... :-) ). I am using an existing theory that runs well under Isabelle 2009-2, but it does not on Isabelle 2012. I am trying to make it work on this version, but I am finding some problems and although I have been looking for there is not too much documentation.

In particular I am having parsing errors on some statements using "types"

In the 2009 version the code is like this:
types type8 ="type_length8 Word"
translations (type) "type8" <= (type) "type_length8 word"

It seems that this is not available anymore. I have replaced "types" by "type_synonym", are types and type_synonym equivalent?

Once modified this, this theory imports "Enum" theory. Again, this is not a problem in Isabelle 2009-2, but Isabelle 2012 loads its own Enum theory. Is it possible not to load "Enum" in Isabelle 2012 so I can use the Non-Isabelle theory?? or should I have to rename the theory, and probably also the class enum?

Thank you for your help,

David Sanán.









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