Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy



On Wed, 22 May 2013, Christoph LANGE wrote:

Well, but there _is_ a notion of "programming" in Isabelle, given that
it is based on a functional programming language, isn't it?

You need to be specific what you mean by "Isabelle".  Maybe Isabelle/HOL?

In some sense, generic "Isabelle" is a framework (or playground) for a multitude of formal languages of different use and purpose: Isabelle/ML, Isabelle/Scala, Isabelle/Pure, Isabelle/HOL, Isabelle/Isar, Isabelle/XYZ.

See also https://sites.google.com/site/isabelleedinburgh2013/Slides_makarius.pdf?attredirects=0 notably slide 4 about *some* languages of Isabelle.


	Makarius




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