Re: [isabelle] command "types" on Isabelle 2012



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.

--
  Peter

On Fr, 2012-12-14 at 12:41 +0100, Lars Noschinski wrote:
> 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







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