[isabelle-dev] Duplicate theory??

[Lawrence Paulson]

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?

Larry

> 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.)