Skip to content

Commit

Permalink
Merge pull request #89 from yiyuan-cao/patch-1
Browse files Browse the repository at this point in the history
Update README of Proofrecording
  • Loading branch information
jrh13 authored Feb 22, 2024
2 parents ea45176 + cee131d commit 4393d50
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions Proofrecording/README
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
**** EXPORTATION TO COQ ****
**** ****
**** Steven Obua ([email protected]) ****
**** Technische Universit�t M�nchen ****
**** Technische Universität München ****
**** February 2005 ****
**** and ****
**** Chantal Keller ([email protected])****
Expand Down Expand Up @@ -165,7 +165,7 @@ subdirectory $HOLPROOFEXPORTDIR/hollight/hollight.

4. To exploit the theorems that have been exported, you have to download
the Coq's interface at
<http://perso.ens-lyon.fr/chantal.keller/Documents-recherche/Stage09/hollightcoq-coq.tar.gz>.
<https://www.lri.fr/~keller/Documents-recherche/Stage09/hollightcoq-all.tar.gz>.
A README file explains how to use it.


Expand Down

0 comments on commit 4393d50

Please sign in to comment.