aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/example.v
Commit message (Expand)AuthorAge
* - update coq exampleGravatar Hendrik Tews2013-05-14
* CommentsGravatar David Aspinall2009-12-01
* Remove more of 80 codeGravatar David Aspinall2009-09-08
* Added Module/EndGravatar David Aspinall2005-11-25
* Update to Coq 8.0 syntaxGravatar David Aspinall2004-04-22
* Update for V8 syntax.Gravatar David Aspinall2004-04-21
* Use official indentation\!Gravatar David Aspinall2004-04-02
* Rever to simplest exampleGravatar David Aspinall2003-10-05
* code cleaning + deals better with the new module system of Coq. DidGravatar Pierre Courtieu2003-02-03
* Added a file for testing modules of coq (new version 7.4). Plus someGravatar Pierre Courtieu2003-01-29
* Modifications for support of Coq-7.3.1+ and above (new module system).Gravatar Pierre Courtieu2003-01-24
* WhitespaceGravatar David Aspinall2002-01-16
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 01:22:00 +0000