[isabelle-dev] Duplicate theory??

Lawrence Paulson lp15 at cam.ac.uk
Fri Apr 5 16:48:28 CEST 2019

Can I leave this with you then?

Let me know if you are successful. Perhaps this tiny theory could be eliminated altogether. What is the point of defining the syntax separate from the semantics?


> On 5 Apr 2019, at 15:33, Traytel Dmitriy <traytel at inf.ethz.ch> wrote:
> I produced a patch, but run into the problem Jasmin reported today when trying to test it. (I'll write more in the other thread.)

More information about the isabelle-dev mailing list