--- a/src/Doc/manual.bib Tue Mar 29 23:45:28 2016 +0200
+++ b/src/Doc/manual.bib Wed Mar 30 15:16:50 2016 +0200
@@ -333,6 +333,12 @@
note = {\url{http://isabelle.in.tum.de/doc/sledgehammer.pdf}}
}
+@manual{isabelle-corec,
+ author = {Jasmin Christian Blanchette and Andreas Lochbihler and Andrei Popescu and Dmitriy Traytel},
+ title = {Defining Nonprimitively Corecursive Functions in {Isabelle\slash HOL}},
+ institution = {TU Munich},
+ note = {\url{http://isabelle.in.tum.de/doc/corec.pdf}}}
+
@inproceedings{blanchette-nipkow-2010,
title = "Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder",
author = "Jasmin Christian Blanchette and Tobias Nipkow",
@@ -352,11 +358,11 @@
publisher = {Springer}
}
-@inproceedings{blanchette-et-al-2015-corec,
+@inproceedings{blanchette-et-al-2015-fouco,
author = {Jasmin Christian Blanchette and
Andrei Popescu and
Dmitriy Traytel},
- title = {Foundational extensible corecursion: a proof assistant perspective},
+ title = {Foundational extensible corecursion: A proof assistant perspective},
booktitle = {20th {ACM} {SIGPLAN} International Conference on
Functional Programming, {ICFP} 2015},
pages = {192--204},
@@ -366,6 +372,15 @@
publisher = {{ACM}},
}
+@misc{blanchette-et-al-2016-fouco2,
+ author = {Jasmin Christian Blanchette and
+ Andreas Lochbihler and
+ Andrei Popescu and
+ Dmitriy Traytel},
+ title = {Productivity for free: Friendly Corecursion for {Isabelle\slash HOL}},
+ howpublished = "\url{http://www21.in.tum.de/~blanchet/fouco2.pdf}",
+ year = 2016}
+
@inproceedings{blanchette-et-al-2014-impl,
author = "Jasmin Christian Blanchette and Johannes H{\"o}lzl
and Andreas Lochbihler and Lorenz Panny and Andrei Popescu and Dmitriy Traytel",