aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Logic/WKL.v
Commit message (Collapse)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
|
* Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.Gravatar Hugo Herbelin2015-12-10
| | | | Marking it as experimental.
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Added an arithmetical characterization of the hypothesis of WKL.Gravatar Hugo Herbelin2014-12-01
|
* Completing c236b51348d2 by fixing EqdepFactsv actually committing theGravatar Hugo Herbelin2014-07-17
new files (WeakFan.v and WKL.v).