Re: [isabelle] Quotients of nominal types



On Mon, 12 Aug 2013, Christian Urban wrote:

There is no way, I think, to lift/transfer theorems by names (on the non-ML-level).

Reading this 2 or 3 times, I still don't understand what is meant -- too many negations.


Isabelle has many different languages of different kind and purpose: Isabelle/ML, Isabelle/Isar, Isabelle/Scala, Isabelle/Pure, Isabelle/HOL, Isabelle/latex document source etc.

It does not make any sense to speak about "levels" here, and Isabelle/ML vs. Isabelle/Isar are particularly difficult to arrange in 2-dimensional topology. In reality it probably looks more like a Klein bottle.

To understand how Isabelle works, one needs to get basic terminology right, and maybe spend some efforts to stop using wrong expressions.


	Makarius





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