# HG changeset patch
# User haftmann
# Date 1377080914 -7200
# Node ID f4c6f8f6515b2faf650c43a6f835af7f42e97262
# Parent  9ae9bbaccee1fef2d45f85590d6c395a49ec8592
reference to datatype refinment paper

diff -r 9ae9bbaccee1 -r f4c6f8f6515b src/Doc/Codegen/Refinement.thy
--- 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"});
diff -r 9ae9bbaccee1 -r f4c6f8f6515b src/Doc/manual.bib
--- 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}},