--- a/src/Doc/Codegen/Refinement.thy Wed Aug 21 10:58:15 2013 +0200
+++ b/src/Doc/Codegen/Refinement.thy Wed Aug 21 12:28:34 2013 +0200
@@ -264,6 +264,9 @@
*}
text {*
+ See further \cite{Haftmann-Kraus-Kuncar-Nipkow:2013:data_refinement}
+ for the meta theory of datatype refinement involving invariants.
+
Typical data structures implemented by representations involving
invariants are available in the library, theory @{theory Mapping}
specifies key-value-mappings (type @{typ "('a, 'b) mapping"});
--- a/src/Doc/manual.bib Wed Aug 21 10:58:15 2013 +0200
+++ b/src/Doc/manual.bib Wed Aug 21 12:28:34 2013 +0200
@@ -629,15 +629,16 @@
%H
-@InProceedings{Haftmann-Wenzel:2006:classes,
- author = {Florian Haftmann and Makarius Wenzel},
- title = {Constructive Type Classes in {Isabelle}},
- editor = {T. Altenkirch and C. McBride},
- booktitle = {Types for Proofs and Programs, TYPES 2006},
- publisher = {Springer},
- series = {LNCS},
- volume = {4502},
- year = {2007}
+@inproceedings{Haftmann-Kraus-Kuncar-Nipkow:2013:data_refinement,
+ author = {Florian Haftmann and Alexander Krauss and Ond\v{r}ej Kun\v{c}ar and Tobias Nipkow},
+ title = {Data Refinement in Isabelle/HOL},
+ booktitle = {Interactive Theorem Proving (ITP 2013)},
+ pages = {100-115},
+ year = 2013,
+ publisher = Springer,
+ series = {Lecture Notes in Computer Science},
+ volume = {7998},
+ editor = {S. Blazy and C. Paulin-Mohring and D. Pichardie}
}
@inproceedings{Haftmann-Nipkow:2010:code,
@@ -651,6 +652,17 @@
volume = 6009
}
+@InProceedings{Haftmann-Wenzel:2006:classes,
+ author = {Florian Haftmann and Makarius Wenzel},
+ title = {Constructive Type Classes in {Isabelle}},
+ editor = {T. Altenkirch and C. McBride},
+ booktitle = {Types for Proofs and Programs, TYPES 2006},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = {4502},
+ year = {2007}
+}
+
@InProceedings{Haftmann-Wenzel:2009,
author = {Florian Haftmann and Makarius Wenzel},
title = {Local theory specifications in {Isabelle/Isar}},