[isabelle-dev] Confusion about ML_file and SML_file

2017-06-27 Thread Wenda Li
Dear Isabelle developers, When I am porting some of my old code from Isabelle-2016 to Isabelle2016-1, I have encountered a problem that the command “SML_file" does not accept a SML file that contains the function “PolyML.IntInf.gcd”. By going through NEWS, I found the following entry: *

Re: [isabelle-dev] Confusion about ML_file and SML_file

2017-06-27 Thread Makarius
On 27/06/17 22:21, Wenda Li wrote: > Dear Isabelle developers, > > When I am porting some of my old code from Isabelle-2016 to Isabelle2016-1, I > have encountered a problem that the command “SML_file" does not accept a SML > file that contains the function “PolyML.IntInf.gcd”. By going through