aboutsummaryrefslogtreecommitdiff
path: root/coq/example.v
AgeCommit message (Expand)Author
2013-05-14- update coq exampleHendrik Tews
2009-12-01CommentsDavid Aspinall
2009-09-08Remove more of 80 codeDavid Aspinall
2005-11-25Added Module/EndDavid Aspinall
2004-04-22Update to Coq 8.0 syntaxDavid Aspinall
2004-04-21Update for V8 syntax.David Aspinall
2004-04-02Use official indentation\!David Aspinall
2003-10-05Rever to simplest exampleDavid Aspinall
2003-02-03code cleaning + deals better with the new module system of Coq. DidPierre Courtieu
2003-01-29Added a file for testing modules of coq (new version 7.4). Plus somePierre Courtieu
2003-01-24Modifications for support of Coq-7.3.1+ and above (new module system).Pierre Courtieu
2002-01-16WhitespaceDavid Aspinall
2000-06-08proper indentation;Makarius Wenzel
1999-11-13Use infix syntaxDavid Aspinall
1999-10-06Remove coq-Search function, now generic.David Aspinall
1999-09-24unified example with other proof assistants;Makarius Wenzel
1999-09-13Cleaned up example files so all demonstrate same theorem "conj_comms".David Aspinall
1999-08-23Updated from Coq 6.3 distrib.David Aspinall
1999-08-23Updates suggested by Markus and Patrick for Coq 6.3.David Aspinall
1998-10-02changed maintainer information to lego@dcs and isabelle@dcs .Thomas Kleymann
1998-10-01Updated maintainer tags to remove lego email address.David Aspinall
1998-09-23Example file suggested by Healf.David Aspinall
1998-09-09Added Id to headers.David Aspinall
1998-09-03Added Isabelle example and skeleton for Coq and Lego.David Aspinall
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:45:49 +0000