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



2013-05-22 14:26 Lawrence Paulson:
> Coq and Isabelle/HOL are proof assistants, not programming languages. I can't imagine what gave you that idea. In Coq and Isabelle/HOL you write specifications, not code.

Well, but there _is_ a notion of "programming" in Isabelle, given that
it is based on a functional programming language, isn't it?  I recall
this earlier discussion on the title of the "programming and proving"
tutorial:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-November/msg00148.html

Cheers,

Christoph

-- 
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701

→ Intelligent Computer Mathematics, 8–12 July, Bath, UK.
  Work-in-progress deadline 7 June; http://cicm-conference.org/2013/
→ OpenMath Workshop, 10 July, Bath, UK.
  Submission deadline 7 June; http://cicm-conference.org/2013/openmath/




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