Re: [isabelle] Clone detection for Isabelle theories

> I think your mental model of Isabelle is slightly off. There's no point
> in discussing the design decisions made decades ago when we're really
> discussing how clone detection works with the system we have right now.
> To rephrase: Isabelle has arbitrary user-extensible syntax and it has
> arbitrary executable ML code. If you want to do realistic syntax
> analysis today you have to accept that.

Sorry, that probably came off harsher than intended. I was trying to say
that Isabelle supports all these things today and there is no reliable
way to turn them off.

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