aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/example.v
Commit message (Expand)AuthorAge
* proper indentation;Gravatar Makarius Wenzel2000-06-08
* Use infix syntaxGravatar David Aspinall1999-11-13
* Remove coq-Search function, now generic.Gravatar David Aspinall1999-10-06
* unified example with other proof assistants;Gravatar Makarius Wenzel1999-09-24
* Cleaned up example files so all demonstrate same theorem "conj_comms".Gravatar David Aspinall1999-09-13
* Updated from Coq 6.3 distrib.Gravatar David Aspinall1999-08-23
* Updates suggested by Markus and Patrick for Coq 6.3.Gravatar David Aspinall1999-08-23
* changed maintainer information to lego@dcs and isabelle@dcs .Gravatar Thomas Kleymann1998-10-02
* Updated maintainer tags to remove lego email address.Gravatar David Aspinall1998-10-01
* Example file suggested by Healf.Gravatar David Aspinall1998-09-23
* Added Id to headers.Gravatar David Aspinall1998-09-09
* Added Isabelle example and skeleton for Coq and Lego.Gravatar David Aspinall1998-09-03