index
:
proof-general
master
Emacs interface for proof assistants
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
coq
/
example.v
Commit message (
Expand
)
Author
Age
*
- update coq example
Hendrik Tews
2013-05-14
*
Comments
David Aspinall
2009-12-01
*
Remove more of 80 code
David Aspinall
2009-09-08
*
Added Module/End
David Aspinall
2005-11-25
*
Update to Coq 8.0 syntax
David Aspinall
2004-04-22
*
Update for V8 syntax.
David Aspinall
2004-04-21
*
Use official indentation\!
David Aspinall
2004-04-02
*
Rever to simplest example
David Aspinall
2003-10-05
*
code cleaning + deals better with the new module system of Coq. Did
Pierre Courtieu
2003-02-03
*
Added a file for testing modules of coq (new version 7.4). Plus some
Pierre Courtieu
2003-01-29
*
Modifications for support of Coq-7.3.1+ and above (new module system).
Pierre Courtieu
2003-01-24
*
Whitespace
David Aspinall
2002-01-16
*
proper indentation;
Makarius Wenzel
2000-06-08
*
Use infix syntax
David Aspinall
1999-11-13
*
Remove coq-Search function, now generic.
David Aspinall
1999-10-06
*
unified example with other proof assistants;
Makarius Wenzel
1999-09-24
*
Cleaned up example files so all demonstrate same theorem "conj_comms".
David Aspinall
1999-09-13
*
Updated from Coq 6.3 distrib.
David Aspinall
1999-08-23
*
Updates suggested by Markus and Patrick for Coq 6.3.
David Aspinall
1999-08-23
*
changed maintainer information to lego@dcs and isabelle@dcs .
Thomas Kleymann
1998-10-02
*
Updated maintainer tags to remove lego email address.
David Aspinall
1998-10-01
*
Example file suggested by Healf.
David Aspinall
1998-09-23
*
Added Id to headers.
David Aspinall
1998-09-09
*
Added Isabelle example and skeleton for Coq and Lego.
David Aspinall
1998-09-03