diff --git a/thys/Optics/Prisms.thy b/thys/Optics/Prisms.thy
--- a/thys/Optics/Prisms.thy
+++ b/thys/Optics/Prisms.thy
@@ -1,152 +1,152 @@
 section \<open>Prisms\<close>
 
 theory Prisms
   imports Lenses
 begin
 
 subsection \<open> Signature and Axioms \<close>
 
-text \<open>Prisms are like lenses, but they act on sum types rather than product types. For now
-  we do not support many properties about them. See \url{https://hackage.haskell.org/package/lens-4.15.2/docs/Control-Lens-Prism.html}
+text \<open>Prisms are like lenses, but they act on sum types rather than product types~\cite{Gibbons17}. 
+  See \url{https://hackage.haskell.org/package/lens-4.15.2/docs/Control-Lens-Prism.html}
   for more information.\<close>
 
 record ('v, 's) prism =
   prism_match :: "'s \<Rightarrow> 'v option" ("match\<index>")
   prism_build :: "'v \<Rightarrow> 's" ("build\<index>")
 
 type_notation
   prism (infixr "\<Longrightarrow>\<^sub>\<triangle>" 0)
 
 locale wb_prism =
   fixes x :: "'v \<Longrightarrow>\<^sub>\<triangle> 's" (structure)
   assumes match_build: "match (build v) = Some v"
   and build_match: "match s = Some v \<Longrightarrow> s = build v"
 begin
 
   lemma build_match_iff: "match s = Some v \<longleftrightarrow> s = build v"
     using build_match match_build by blast
 
   lemma range_build: "range build = dom match"
     using build_match match_build by fastforce
 end
 
 declare wb_prism.match_build [simp]
 declare wb_prism.build_match [simp]
 
 subsection \<open> Co-dependence \<close>
 
 text \<open> The relation states that two prisms construct disjoint elements of the source. This
   can occur, for example, when the two prisms characterise different constructors of an
   algebraic datatype. \<close>
 
 definition prism_diff :: "('a \<Longrightarrow>\<^sub>\<triangle> 's) \<Rightarrow> ('b \<Longrightarrow>\<^sub>\<triangle> 's) \<Rightarrow> bool" (infix "\<nabla>" 50) where
 "prism_diff X Y = (range build\<^bsub>X\<^esub> \<inter> range build\<^bsub>Y\<^esub> = {})"
 
 lemma prism_diff_intro:
   "(\<And> s\<^sub>1 s\<^sub>2. build\<^bsub>X\<^esub> s\<^sub>1 = build\<^bsub>Y\<^esub> s\<^sub>2 \<Longrightarrow> False) \<Longrightarrow> X \<nabla> Y"
   by (auto simp add: prism_diff_def)
 
 lemma prism_diff_irrefl: "\<not> X \<nabla> X"
   by (simp add: prism_diff_def)
 
 lemma prism_diff_sym: "X \<nabla> Y \<Longrightarrow> Y \<nabla> X"
   by (auto simp add: prism_diff_def)
 
 lemma prism_diff_build: "X \<nabla> Y \<Longrightarrow> build\<^bsub>X\<^esub> u \<noteq> build\<^bsub>Y\<^esub> v"
   by (simp add: disjoint_iff_not_equal prism_diff_def)
 
 subsection \<open> Summation \<close>
 
 definition prism_plus :: "('a \<Longrightarrow>\<^sub>\<triangle> 's) \<Rightarrow> ('b \<Longrightarrow>\<^sub>\<triangle> 's) \<Rightarrow> 'a + 'b \<Longrightarrow>\<^sub>\<triangle> 's" (infixl "+\<^sub>\<triangle>" 85) 
   where
 "X +\<^sub>\<triangle> Y = \<lparr> prism_match = (\<lambda> s. case (match\<^bsub>X\<^esub> s, match\<^bsub>Y\<^esub> s) of
                                  (Some u, _) \<Rightarrow> Some (Inl u) |
                                  (None, Some v) \<Rightarrow> Some (Inr v) |
                                  (None, None) \<Rightarrow> None),
            prism_build = (\<lambda> v. case v of Inl x \<Rightarrow> build\<^bsub>X\<^esub> x | Inr y \<Rightarrow> build\<^bsub>Y\<^esub> y) \<rparr>"
 
 subsection \<open> Instances \<close>
 
 definition prism_suml :: "('a, 'a + 'b) prism" ("Inl\<^sub>\<triangle>") where
 [lens_defs]: "prism_suml = \<lparr> prism_match = (\<lambda> v. case v of Inl x \<Rightarrow> Some x | _ \<Rightarrow> None), prism_build = Inl \<rparr>"
 
 definition prism_sumr :: "('b, 'a + 'b) prism" ("Inr\<^sub>\<triangle>") where
 [lens_defs]: "prism_sumr = \<lparr> prism_match = (\<lambda> v. case v of Inr x \<Rightarrow> Some x | _ \<Rightarrow> None), prism_build = Inr \<rparr>"
 
 lemma wb_prim_suml: "wb_prism Inl\<^sub>\<triangle>"
   apply (unfold_locales)
    apply (simp_all add: prism_suml_def sum.case_eq_if)
   apply (metis option.inject option.simps(3) sum.collapse(1))
   done
 
 lemma wb_prim_sumr: "wb_prism Inr\<^sub>\<triangle>"
   apply (unfold_locales)
    apply (simp_all add: prism_sumr_def sum.case_eq_if)
   apply (metis option.distinct(1) option.inject sum.collapse(2))
   done
 
 lemma prism_suml_indep_sumr [simp]: "Inl\<^sub>\<triangle> \<nabla> Inr\<^sub>\<triangle>"
   by (auto simp add: prism_diff_def lens_defs)
 
 subsection \<open> Lens correspondence \<close>
 
 text \<open> Every well-behaved prism can be represented by a partial bijective lens. We prove 
   this by exhibiting conversion functions and showing they are (almost) inverses. \<close>
 
 definition prism_lens :: "('a, 's) prism \<Rightarrow> ('a \<Longrightarrow> 's)" where
 "prism_lens X = \<lparr> lens_get = (\<lambda> s. the (match\<^bsub>X\<^esub> s)), lens_put = (\<lambda> s v. build\<^bsub>X\<^esub> v) \<rparr>"
 
 definition lens_prism :: "('a \<Longrightarrow> 's) \<Rightarrow> ('a, 's) prism" where
 "lens_prism X = \<lparr> prism_match = (\<lambda> s. if (s \<in> \<S>\<^bsub>X\<^esub>) then Some (get\<^bsub>X\<^esub> s) else None)
                 , prism_build = create\<^bsub>X\<^esub> \<rparr>"
 
 lemma get_prism_lens: "get\<^bsub>prism_lens X\<^esub> = the \<circ> match\<^bsub>X\<^esub>"
   by (simp add: prism_lens_def fun_eq_iff)
 
 lemma src_prism_lens: "\<S>\<^bsub>prism_lens X\<^esub> = range (build\<^bsub>X\<^esub>)"
   by (auto simp add: prism_lens_def lens_source_def)
 
 lemma create_prism_lens: "create\<^bsub>prism_lens X\<^esub> = build\<^bsub>X\<^esub>"
   by (simp add: prism_lens_def lens_create_def fun_eq_iff)
 
 lemma prism_lens_inverse:
   "wb_prism X \<Longrightarrow> lens_prism (prism_lens X) = X"
   unfolding lens_prism_def src_prism_lens create_prism_lens get_prism_lens
   by (auto intro: prism.equality simp add: fun_eq_iff domIff wb_prism.range_build)
 
 text \<open> Function @{const lens_prism} is almost inverted by @{const prism_lens}. The $put$
   functions are identical, but the $get$ functions differ when applied to a source where
   the prism @{term X} is undefined. \<close>
 
 lemma lens_prism_put_inverse:
   "pbij_lens X \<Longrightarrow> put\<^bsub>prism_lens (lens_prism X)\<^esub> = put\<^bsub>X\<^esub>"
   unfolding prism_lens_def lens_prism_def
   by (auto simp add: fun_eq_iff pbij_lens.put_is_create)
 
 lemma wb_prism_implies_pbij_lens:
   "wb_prism X \<Longrightarrow> pbij_lens (prism_lens X)"
   by (unfold_locales, simp_all add: prism_lens_def)
 
 lemma pbij_lens_implies_wb_prism:
   assumes "pbij_lens X" 
   shows "wb_prism (lens_prism X)"
 proof (unfold_locales)
   fix s v
   show "match\<^bsub>lens_prism X\<^esub> (build\<^bsub>lens_prism X\<^esub> v) = Some v"
     by (simp add: lens_prism_def weak_lens.create_closure assms)
   assume a: "match\<^bsub>lens_prism X\<^esub> s = Some v"
   show "s = build\<^bsub>lens_prism X\<^esub> v"
   proof (cases "s \<in> \<S>\<^bsub>X\<^esub>")
     case True
     with a assms show ?thesis 
       by (simp add: lens_prism_def lens_create_def, 
           metis mwb_lens.weak_get_put pbij_lens.put_det pbij_lens_mwb)
   next
     case False
     with a assms show ?thesis by (simp add: lens_prism_def)
   qed
 qed
 
 ML_file \<open>Prism_Lib.ML\<close>
 
 end
diff --git a/thys/Optics/document/root.bib b/thys/Optics/document/root.bib
--- a/thys/Optics/document/root.bib
+++ b/thys/Optics/document/root.bib
@@ -1,376 +1,384 @@
 @InProceedings{Alkassar2008,
 author="Alkassar, E. and Hillebrand, M. and Leinenbach, D. and Schirmer, N. and Starostin, A.",
 title="The {Verisoft} Approach to Systems Verification",
 booktitle="VSTTE 2008",
 year="2008",
 publisher="Springer",
 pages="209--224",
 series="LNCS",
 volume="5295"
 }
 
 @InProceedings{Armstrong2012,
   Title                    = {Automated Reasoning in Higher-Order Regular Algebra},
   Author                   = {Armstrong, A. and Struth, G.},
   Booktitle                = {RAMiCS 2012},
   Year                     = {2012},
   Month                    = {September},
   Publisher                = {Springer},
   Series                   = {LNCS},
   Volume                   = {7560}
 }
 
 @InProceedings{Armstrong2013,
   Title                    = {Program Analysis and Verification Based on {Kleene Algebra} in {Isabelle/HOL}},
   Author                   = {Armstrong, A. and Struth, G. and Weber, T.},
   Booktitle                = {ITP},
   Year                     = 2013,
   Publisher                = {Springer},
   Series                   = {LNCS},
   Volume                   = 7998
 }
 
 @Article{Armstrong2015,
   author="Armstrong, A. and Gomes, V. and Struth, G.",
   title="Building program construction and verification tools from algebraic principles",
   journal="Formal Aspects of Computing",
   year="2015",
   volume="28",
   number="2",
   pages="265--293"
 }
 
 @Book{Back1998,
   author =    {Back, R.-J. and von Wright, J.},
   title =        {Refinement Calculus: A Systematic Introduction},
   publisher =    {Springer},
   year =         1998}
 
 @inproceedings{Back2003,
  author = {Back, R.-J. and Preoteasa, V.},
  title = {Reasoning About Recursive Procedures with Parameters},
  booktitle = {Proc. Workshop on Mechanized Reasoning About Languages with Variable Binding},
  series = {MERLIN '03},
  year = {2003},
  location = {Uppsala, Sweden},
  pages = {1--7},
  publisher = {ACM}
 } 
 
 
 @InProceedings{Blanchette2011,
   Title                    = {Automatic Proof and Disproof in {Isabelle/HOL}},
   Author                   = {Blanchette, J. C. and Bulwahn, L. and Nipkow, T.},
   Booktitle                = {FroCoS},
   Year                     = {2011},
   Pages                    = {12--27},
   Publisher                = {Springer},
   Series                   = {LNCS},
   Volume                   = {6989}
 }
 
 @INPROCEEDINGS{Calcagno2007, 
 author={Calcagno, C. and O'Hearn, P. and Yang, H.}, 
 booktitle={LICS}, 
 title={Local Action and Abstract Separation Logic}, 
 year={2007}, 
 pages={366--378}, 
 month={July},
 publisher={IEEE}}
 
 @INCOLLECTION{Cavalcanti&06,
   KEY           = "Cavalcanti\&06",
   AUTHOR        = {Cavalcanti, A. and Woodcock, J.},
   TITLE         = {A Tutorial Introduction to {CSP} in Unifying Theories of
                    Programming},
   BOOKTITLE     = {Refinement Techniques in Software Engineering},
   SERIES        = {LNCS},
   PUBLISHER     = {Springer},
   ISBN          = {978-3-540-46253-8},
   PAGES         = {220--268},
   VOLUME        = {3167},
   YEAR          = {2006},
   COMMENT       = "BIB PGL"}
 
 @inproceedings{Dongol15,
   author    = {Dongol, B. and
                Gomes, V. and
                Struth, G.},
   title     = {A Program Construction and Verification Tool for Separation Logic},
   booktitle = {{MPC} 2015},
   series    = {LNCS},
   volume    = {9129},
   pages     = {137--158},
   publisher = {Springer},
   year      = {2015}
 }
 
 @InProceedings{Feliachi2010,
   author =       {Feliachi, A. and Gaudel, M.-C. and Wolff, B.},
   title =        {Unifying Theories in {Isabelle/HOL}},
   booktitle    = {UTP 2010},
   pages    =     {188--206},
   year =         2010,
   volume    =    6445,
   series =       {LNCS},
   publisher = {Springer}}
 
 @InProceedings{Feliachi2012,
   author =       {Feliachi, A. and Gaudel, M.-C. and Wolff, B.},
   title =        {{Isabelle/Circus}: a Process Specification and
                   Verification Environment},
   booktitle    = {VSTTE 2012},
   pages    =     {243--260},
   year =         2012,
   volume    =    7152,
   series =       {LNCS},
   publisher = {Springer}}
 
 @InProceedings{Fischer2015,
 author="Fischer, S. and Hu, Z. and Pacheco, H.",
 title="A Clear Picture of Lens Laws",
 booktitle="MPC 2015",
 year="2015",
 publisher="Springer",
 pages="215--223",
 }
 
 @PhdThesis{Foster09,
   author =       {Foster, J.},
   title =        {Bidirectional programming languages},
   school =       {University of Pennsylvania},
   year =         2009}
 
 @article{Foster07,
  author = {Foster, J. and Greenwald, M. and Moore, J. and Pierce, B. and Schmitt, A.},
  title = {Combinators for Bidirectional Tree Transformations: A Linguistic Approach to the View-update Problem},
  journal = {ACM Trans. Program. Lang. Syst.},
  issue_date = {May 2007},
  volume = {29},
  number = {3},
  month = may,
  year = {2007},
  issn = {0164-0925},
  articleno = {17},
  url = {http://doi.acm.org/10.1145/1232420.1232424},
  doi = {10.1145/1232420.1232424},
  acmid = {1232424},
  publisher = {ACM},
  address = {New York, NY, USA},
  keywords = {Bidirectional programming, Harmony, XML, lenses, view update problem},
 } 
 
 @InProceedings{Foster11,
   Title                    = {Automated Engineering of Relational and Algebraic Methods in {Isabelle/HOL}},
   Author                   = {Foster, S. and Struth, G. and Weber, T.},
   Booktitle                = {RAMICS 2011},
   Year                     = {2011},
   Pages                    = {52--67},
   Publisher                = {Springer},
   Series                   = {LNCS},
   Volume                   = {6663},
   ISBN                     = {978-3-642-21069-3}
 }
 
 @InProceedings{Foster14,
   Title                    = {{Isabelle/UTP}: A Mechanised Theory Engineering Framework},
   Author                   = {Foster, S. and Zeyda, F. and Woodcock, J.},
   Booktitle                = {UTP},
   Year                     = {2014},
   Pages                    = {21--41},
   Publisher                = {Springer},
   Series                   = {LNCS},
   Volume                   = {8963}
 }
 
 @InProceedings{Foster16a,
   author =       {Foster, S. and Zeyda, F. and Woodcock, J.},
   title =        {Unifying heterogeneous state-spaces with lenses},
   booktitle =    {Proc. 13th Intl. Conf. on Theoretical Aspects of Computing (ICTAC)},
   year =         2016,
   volume =    9965,
   series =       {LNCS},
   publisher =    {Springer}}
 
 @InProceedings{Foster16b,
   author =       {Foster, S. and Thiele, B. and Cavalcanti, A. and Woodcock, J.},
   title =        {Towards a {UTP} semantics for {Modelica}},
   booktitle =    {Proc. 6th Intl. Symp. on Unifying Theories of Programming},
   month =        {June},
   year =         2016,
   series =       {LNCS},
   volume =       {10134},
   publisher =    {Springer}
 }
 
+@Article{Foster2020-IsabelleUTP,
+  author =       {Foster, S. and Baxter, J. and Cavalcanti, A. and Woodcock, J. and Zeyda, F.},
+  title =        {Unifying Semantic Foundations for Automated Verification Tools in {Isabelle/UTP}},
+  journal =      {Science of Computer Programming},
+  volume =       {197},
+  month =        {October},
+  year =         {2020}}
+
 @article{Gibbons17,
   title = "Profunctor Optics: Modular Data Accessors",
   author = "Matthew Pickering and Jeremy Gibbons and Nicolas Wu",
   year = "2017",
   journal = "The Art, Science, and Engineering of Programming",
   number = "2",
   publisher = "AOSA",
   url = "http://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/poptics.pdf",
   volume = "1",
 }
 
 @Book{Hehner93,
   Title                    = {A Practical Theory of Programming},
   Author                   = {E. C. R. Hehner},
   Publisher                = {Springer},
   Year                     = {1993}
 }
 
 @Book{Hoare85,
   Title                    = {{Communicating Sequential Processes}},
   Author                   = {Hoare, T.},
   Publisher                = {Prentice-Hall},
   Year                     = {1985},
   Size                     = {256}
 }
 
 @ARTICLE{Hoare87,
   AUTHOR        = "Hoare, T. and Hayes, I. and He, J.
                    and Morgan, C. and Roscoe, A. and Sanders, J.
                    and S{\o}rensen, I. and Spivey, J. and Sufrin, B.",
   TITLE         = "The Laws of Programming",
   JOURNAL       = "Communications of the ACM",
   VOLUME        = "30",
   NUMBER        = "8",
   PAGES         = "672--687",
   MONTH         = "August",
   YEAR          = "1987"}
 
 @Book{Hoare&98,
   Title                    = {Unifying {Theories} of {Programming}},
   Author                   = {Hoare, T. and He, J.},
   Publisher                = {Prentice-Hall},
   Year                     = {1998},
   ISBN                     = {ISBN-10: 0134587618},
   Comment                  = {NA PGL},
   Key                      = {Hoare\&98}
 }
 
 @InProceedings{Hofmann2011,
   Title                    = {Symmetric lenses},
   Author                   = {Hofmann, M. and Pierce, B. and Wagner, D.},
   Booktitle                = {POPL},
   Year                     = {2011},
   Pages                    = {371--384},
   Publisher                = {IEEE}
 }
 
 @InProceedings{Huffman13,
   Title                    = {Lifting and Transfer: A Modular Design for Quotients in {Isabelle/HOL}},
   Author                   = {Huffman, B. and Kun\v{c}ar, O.},
   Booktitle                = {CPP},
   Year                     = {2013},
   Pages                    = {131--146},
   Publisher                = {Springer},
   Series                   = {LNCS},
   Volume                   = {8307}
 }
 
 @Book{Isabelle,
   Title                    = {{Isabelle/HOL: A Proof Assistant for Higher-Order Logic}},
   Author                   = {Nipkow, T. and Wenzel, M. and Paulson, L. C.},
   Publisher                = {Springer},
   Year                     = {2002},
   Series                   = {LNCS},
   Volume                   = {2283}
 }
 
 @inproceedings{Klein2009,
  author = {Klein, G. and others},
  title = {{seL4}: Formal Verification of an {OS} Kernel},
  booktitle = {Proc. 22nd Symp. on Operating Systems Principles (SOSP)},
  year = {2009},
  pages = {207--220},
  publisher = {ACM}
 } 
 
 @INPROCEEDINGS{Oliveira07,
   author =       {Oliveira, M. and Cavalcanti, A. and Woodcock, J.},
   title =        {{Unifying theories in ProofPower-Z}},
   booktitle =    {UTP 2006},
   pages =        {123--140},
   year =         {2007},
   volume =       {4010},
   series    =    {LNCS},
   publisher    = {Springer}
 }
 
 @ARTICLE{Oliveira&09,
   AUTHOR        = {Oliveira, M. and Cavalcanti, A. and Woodcock, J.},
   TITLE         = "{A UTP semantics for {C}ircus}",
   JOURNAL       = {Formal Aspects of Computing},
   VOLUME        = {21},
   ISSUE         = {1-2},
   YEAR          = {2009},
   PAGES         = {3--32},
   PUBLISHER     = {Springer}}
 
 @inproceedings{Reynolds2002,
  author = {Reynolds, J.},
  title = {Separation Logic: A Logic for Shared Mutable Data Structures},
  booktitle = {LICS 2012},
  year = {2002},
  pages = {55--74},
  publisher = {IEEE Computer Society}
 } 
 
 
 @InProceedings{Schirmer2009,
 title = "State Spaces -- The Locale Way ",
 series = "ENTCS",
 volume = "254",
 pages = "161--179",
 year = "2009",
 booktitle = "SSV 2009",
 author = "Schirmer, N. and Wenzel, M."
 }
 
 @Article{Tarski41,
   author =       {Tarski, A.},
   title =        {On the calculus of relations},
   journal =      {J. Symbolic Logic},
   year =         1941,
   volume =    6,
   number =    3,
   pages =     {73--89}}
 
 @Book{Tarski71,
   author =    {Henkin, L. and Monk, J. and Tarski, A.},
   title =        {Cylindric Algebras, Part I.},
   publisher =    {North-Holland},
   year =         1971}
 
 
 
 @InProceedings{Woodcock2016,
   author =       {Woodcock, J. and Foster, S. and Butterfield, A.},
   title =        {Heterogeneous Semantics and Unifying Theories},
   OPTcrossref =  {},
   OPTkey =       {},
   booktitle =    {7th Intl. Symp. on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA)},
   year =         {2016},
   OPTeditor =    {},
   OPTvolume =    {},
   OPTnumber =    {},
   OPTseries =    {},
   OPTpages =     {},
   OPTmonth =     {},
   OPTaddress =   {},
   OPTorganization = {},
   OPTpublisher = {},
   note =         {To appear},
   OPTannote =    {}
 }
 
 @InProceedings{Zeyda16,
   author =       {Zeyda, F. and Foster, S. and Freitas, L.},
   title =        {An Axiomatic Value Model for {Isabelle/UTP}},
   booktitle =    {Proc. 6th Intl. Symp. on Unifying Theories of Programming},
   year =         2016,
   note =         {To appear}}
 
diff --git a/thys/Optics/document/root.tex b/thys/Optics/document/root.tex
--- a/thys/Optics/document/root.tex
+++ b/thys/Optics/document/root.tex
@@ -1,106 +1,107 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,isabellesym}
 \usepackage{fullpage}
 \usepackage[usenames,dvipsnames]{color}
 \usepackage{graphicx}
 \usepackage{document}
 
 % further packages required for unusual symbols (see also
 % isabellesym.sty), use only when needed
 
 \usepackage{amssymb}
   %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
   %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
   %\<triangleq>, \<yen>, \<lozenge>
 
 \usepackage[greek,english]{babel}
   %option greek for \<euro>
   %option english (default language) for \<guillemotleft>, \<guillemotright>
 
 \usepackage[only,bigsqcap]{stmaryrd}
   %for \<Sqinter>
 
 \usepackage{eufrak}
   %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
 
 %\usepackage{textcomp}
   %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
   %\<currency>
 
 \usepackage{stmaryrd}
 
 % this should be the last package used
 \usepackage{pdfsetup}
 
 % urls in roman style, theory text in math-similar italics
 \urlstyle{rm}
 \isabellestyle{it}
 
 % for uniform font size
 %\renewcommand{\isastyle}{\isastyleminor}
 
 % Lens operations
 
 \newcommand{\view}{\mathit{V}}
 \newcommand{\src}{\mathit{S}}
 \newcommand{\lsbs}{{L}}
 \newcommand{\lput}{\textit{\textsf{put}}}
 \newcommand{\lget}{\textit{\textsf{get}}}
 \newcommand{\lcreate}{\mathit{create}}
 \newcommand{\lto}{\Longrightarrow}
 \newcommand{\lsubseteq}{\preceq}
 \newcommand{\lsupseteq}{\mathop{\supseteq_\lsbs}}
 \newcommand{\lequiv}{\approx}
 \newcommand{\lcomp}{;_\lsbs}
 \newcommand{\lplus}{+_\lsbs}
 \newcommand{\lquot}{\mathop{/\!_\lsbs}}
 \newcommand{\lindep}{\mathop{\,\bowtie\,}}
 \newcommand{\lone}{\mathbf{1}}
 \newcommand{\lzero}{\mathbf{0}}
 \newcommand{\lfst}{\textit{\textsf{\textbf{fst}}}}
 \newcommand{\lsnd}{\textit{\textsf{\textbf{snd}}}}
 
 \setcounter{topnumber}{1}
 \setcounter{bottomnumber}{1}
 \setcounter{totalnumber}{1}
 
 \begin{document}
 
 \title{Optics in Isabelle/HOL}
 
 \author{Simon Foster and Frank Zeyda \\[.5ex] University of York, UK \\[2ex] \texttt{\small $\{$simon.foster,frank.zeyda$\}$@york.ac.uk}}
 
 \maketitle
 
 \begin{abstract}
   Lenses provide an abstract interface for manipulating data types through spatially-separated views. They are defined
   abstractly in terms of two functions, $\lget$, the return a value from the source type, and $\lput$ that updates
   the value. We mechanise the underlying theory of lenses, in terms of an algebraic hierarchy of lenses, including
   well-behaved and very well-behaved lenses, each lens class being characterised by a set of lens laws. We also mechanise 
   a lens algebra in Isabelle that enables their composition and comparison, so as to allow construction of complex lenses.
   This is accompanied by a large library of algebraic laws. Moreover we also show how the lens classes can be applied by 
-  instantiating them with a number of Isabelle data types. This theory development is based on our recent paper~\cite{Foster16a}, which
-  shows how lenses can be used to unify heterogeneous representations of state-spaces in formalised programs.
+  instantiating them with a number of Isabelle data types. This theory development is based on our recent 
+  papers~\cite{Foster16a,Foster2020-IsabelleUTP}, which show how lenses can be used to unify heterogeneous representations 
+  of state-spaces in formalised programs.
 \end{abstract}
 
 \tableofcontents
 
 % sane default for proof documents
 \parindent 0pt\parskip 0.5ex
 
 % generated text of all theories
 \input{session}
 
 \vspace{4ex}
 
 % Acknowledgments 
 \noindent\textbf{Acknowledgements}. This work is partly supported by EU H2020 project \emph{INTO-CPS}, grant agreement
 644047. \url{http://into-cps.au.dk/}. We would also like to thank Prof. Burkhart Wolff and Dr. Achim Brucker
 for their generous and helpful comments on our work, and particurlarly their invaluable advice on Isabelle
 mechanisation and ML coding.
 
 % optional bibliography
 \bibliographystyle{abbrv}
 \bibliography{root}
 
 \end{document}