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
Reading this 2 or 3 times, I still don't understand what is meant -- too
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and