Re: [isabelle] Quotients of nominal types






On Monday, August 12, 2013 at 15:36:27 (+0200), Makarius wrote:
 > 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.

Is there an Academie Isabelle I do not know of yet? ;o)

I can only recommend the interview with Richard Feynman between knowing 
the name of something and knowing something.
  
  http://www.youtube.com/watch?v=05WS0WN7zMQ

So we can talk about Isabelle/ML and be very grateful that it is so smoothly
integreated with everything else. But the fact remains that almost all people 
who want to learn Isabelle do not want to learn anything about ML and its 
poorly documented infrastructure that is called Isabelle distribution. If 
some word signifies this, then I am happy to use it. Knowing how hard it is,
I laud everybody who teaches people knowing something, than knowing a name
for something. Am I already off-topic now....;o) 

Christian






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