Bug#880546: RFP: Isabelle -- generic proof assistant

[GengYu Rao <zouyoo@outlook.com>]

Package: wnpp
Severity: wishlist

* Package name    : Isabelle
    Version         : 2017
    Upstream Author :  University of Cambridge
* URL             : http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html
* License         : BSD-3-Clause
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2017/COPYRIGHT
   Description     :

Isabelle/HOL allows to turn executable specifications directly into code in
SML, OCaml, Haskell, and Scala.
Isabelle comes with a large theory library of formally verified 
mathematics,
including elementary number theory , analysis , algebraand set theory .
Also provided are numerous examples arising from research into formal 
verification.
Isabelle/jEdit is the default user interface and Prover IDE for Isabelle.
you can use it as an IDE for sml:)

btw,This package included many add-on components under contrib/*
as you can see, this package is being actively developed.
http://isabelle.in.tum.de/repos/isabelle

I hope someone may pack this into debian.

Regards,

GengYu Rao