phox

AuthorChristophe Raffalli <christophe.raffalli@univ-savoie.fr>
LicenseLGPL-3.0
Homepagehttps://lama.univ-savoie.fr/~raffalli/phox.html
Issue Trackerhttps://github.com/craff/phox/issues
MaintainerChristophe Raffalli <christophe.raffalli@univ-savoie.fr>
Dependencies
&camlp4
ocamlfind
Availableocaml-version >= "4.02.0"
PublishedSep 29, 2017
Source [http] https://github.com/craff/phox/archive/0.89.170929/phox.tar.gz
75636a8bc92f5336acf5708747ad3872
StatisticsNot installed in the last month.
Edithttps://github.com/ocaml/opam-repository/tree/master/packages/phox/phox.0.89.170929/opam

PhoX is an implementation of Higher Order Logic

Its main charateritics are

  • Tactics such as intro or rewrite can be extended by arbitrary theorems
  • As these tactics are used by the auto tactics, this allows to program the auto tatics.
  • You can produce nice latex documents.
  • doc/library/examples/tutorials are available.
  • ...

Authors:

No package is dependent