Email Gateway (Aug 19 2022 at 09:29): Email Gateway (Aug 19 2022 at 09:29):From: David Sanan <David.Sanan@scss.tcd.ie>
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.
Email Gateway (Aug 19 2022 at 09:30):From: Lars Noschinski <noschinl@in.tum.de>
On 13.12.2012 21:12, David Sanan wrote:
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?
Yes, but type_synonym can only make one synonym at a time.
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?
You will need to rename your Enum theory and also the type class.
-- Lars
Email Gateway (Aug 19 2022 at 09:30):From: David Sanan <David.Sanan@scss.tcd.ie>
I see... I will rename it then. Thank you for your help.
David.
Email Gateway (Aug 19 2022 at 09:30):From: Peter Lammich <lammich@in.tum.de>
Grepping for keywords (Like type_synonym or Enum) in the NEWS-file of
Isabelle-2012 often indicates what was changed and how to port it.
Last updated: Nov 21 2024 at 12:39 UTC