diff --git a/thys/Types_To_Sets_Extension/ETTS/Manual/ETTS_Introduction.thy b/thys/Types_To_Sets_Extension/ETTS/Manual/ETTS_Introduction.thy
--- a/thys/Types_To_Sets_Extension/ETTS/Manual/ETTS_Introduction.thy
+++ b/thys/Types_To_Sets_Extension/ETTS/Manual/ETTS_Introduction.thy
@@ -1,382 +1,384 @@
 (* Title: ETTS/Manual/ETTS_Introduction.thy
    Author: Mihails Milehins
    Copyright 2021 (C) Mihails Milehins
 *)
 
 chapter\<open>ETTS: Reference Manual\<close>
 
 section\<open>Introduction\<close>
 theory ETTS_Introduction
   imports 
     Manual_Prerequisites  
     "HOL-Library.Conditional_Parametricity"
 begin
 
 
 
 subsection\<open>Background\<close>
 
 
 text\<open>
 The \textit{standard library} that is associated with the 
 object logic Isabelle/HOL and provided as a part of 
 the standard distribution of Isabelle \<^cite>\<open>"noauthor_isabellehol_2020"\<close> 
 contains a significant number of formalized results from a 
 variety of fields of mathematics (e.g., order theory, algebra, topology). 
 Nevertheless, using the argot that was promoted in the 
 original publication of Types-To-Sets \<^cite>\<open>"blanchette_types_2016"\<close>, 
 the formalization is performed using a type-based approach. 
 Thus, for example, the carrier sets associated with the algebraic structures 
 and the underlying sets of the topological spaces, effectively, 
 consist of all terms of an arbitrary type. This restriction can create 
 an inconvenience when working with mathematical objects induced on a 
 subset of the carrier set/underlying set associated with the original 
 object (e.g., see \<^cite>\<open>"immler_smooth_2019"\<close>).
 
 To address this limitation, several additional libraries were developed 
 upon the foundations of the standard library 
 (e.g., \textit{HOL-Algebra} \<^cite>\<open>"ballarin_isabellehol_2020"\<close> and 
 \textit{HOL-Analysis} \<^cite>\<open>"noauthor_isabellehol_2020-1"\<close>). 
 In terms of the argot associated with Types-To-Sets, these libraries provide 
 the set-based counterparts of many type-based theorems in the standard library,
 along with a plethora of additional results. Nonetheless, the proofs of 
 the majority of the theorems that are available in the standard library 
 are restated explicitly in the libraries that contain the set-based results.
 This unnecessary duplication of efforts is one of the primary problems 
 that the framework Types-To-Sets is meant to address. 
 
 The framework Types-To-Sets offers a unified approach to structuring 
 mathematical knowledge formalized in Isabelle/HOL: potentially, 
 every type-based theorem can be converted to a set-based theorem in 
 a semi-automated manner and the relationship between such type-based 
 and set-based theorems can be articulated clearly and explicitly 
 \<^cite>\<open>"blanchette_types_2016"\<close>. 
 In this document, we describe a particular implementation of the framework 
 Types-To-Sets in Isabelle/HOL that takes the form of a further extension 
 of the language Isabelle/Isar with several new commands and attributes 
 (e.g., see \<^cite>\<open>"wenzel_isabelle/isar_2019-1"\<close>).
 \<close>
 
 
 
 subsection\<open>Prerequisites and conventions\<close>
 
 
 text\<open>
 A reader of this document is assumed to be familiar with 
 the proof assistant Isabelle, the proof language Isabelle/Isar,
 the meta-logic Isabelle/Pure and
 the object logic Isabelle/HOL, as described in, 
 \<^cite>\<open>"paulson_natural_1986" and "wenzel_isabelle/isar_2019-1"\<close>,
 \<^cite>\<open>"bertot_isar_1999" and "wenzel_isabelleisar_2007" and "wenzel_isabelle/isar_2019-1"\<close>,
 \<^cite>\<open>"paulson_foundation_1989" and "wenzel_isabelle/isar_2019-1"\<close> and
 \<^cite>\<open>"yang_comprehending_2017"\<close>, respectively. Familiarity with the
 content of the original articles about Types-To-Sets
 \<^cite>\<open>"blanchette_types_2016" and "kuncar_types_2019"\<close> and
 the first large-scale application of Types-To-Sets
 (as described in \<^cite>\<open>"immler_smooth_2019"\<close>) 
 is not essential but can be useful.
 
 The notational conventions that are used in this document are
 approximately equivalent to the conventions that were suggested in
 \<^cite>\<open>"blanchette_types_2016"\<close>, \<^cite>\<open>"yang_comprehending_2017"\<close> and
 \<^cite>\<open>"kuncar_types_2019"\<close>. 
 However, a disparity comes from our use of explicit notation 
 for the \textit{schematic variables}. In Isabelle/HOL, free variables 
 that occur in the theorems at the top-level in the theory context 
 are generalized implicitly, which may be expressed by replacing 
 fixed variables by schematic variables \<^cite>\<open>"wenzel_isabelle/isar_2001"\<close>. 
 In this article, the schematic variables will be prefixed with the 
 question mark ``$?$'', like so: $?a$. Nonetheless, explicit 
 quantification over the type variables at the top-level 
 is also allowed: $\forall \alpha. \phi\left[\alpha\right]$. 
 Lastly, the square brackets may be used either for the denotation 
 of substitution or to indicate that certain types/terms are a part 
 of a term: $t\left[?\alpha\right]$.
 \<close>
 
 
 
 subsection\<open>Previous work\<close>
 
 
 subsubsection\<open>Relativization Algorithm\label{sec:ra}\<close>
 
 
 text\<open>
 Let ${}_{\alpha}(\beta \approx U)_{\mathsf{Rep}}^{\mathsf{Abs}}$ denote
 \[
 \begin{aligned}
 & (\forall x_{\beta}. \mathsf{Rep}\ x \in U)\ \wedge\\
 & (\forall x_{\beta}. \mathsf{Abs}\ (\mathsf{Rep}\ x) = x)\ \wedge\\
 & (\forall y_{\alpha}. y \in U \longrightarrow \mathsf{Rep}\ (\mathsf{Abs}\ y) = y)
 \end{aligned},
 \]
 let $\rightsquigarrow$ denote the constant/type \textit{dependency relation} 
 (see subsection 2.3 in \<^cite>\<open>"blanchette_types_2016"\<close>), 
 let $\rightsquigarrow^{\downarrow}$ 
 be a \textit{substitutive closure} of the constant/type dependency relation, 
 let $R^{+}$ denote the transitive closure of 
 the binary relation $R$, let $\Delta_c$ denote the set of all types for which 
 $c$ is \textit{overloaded} and let $\sigma\not\leq S $ mean that $\sigma$ is not 
 an instance of any type in $S$ (see \<^cite>\<open>"blanchette_types_2016"\<close> and 
 \<^cite>\<open>"yang_comprehending_2017"\<close>).
 
 The framework Types-To-Sets extends Isabelle/HOL with two axioms: 
 \textit{Local Typedef Rule} (LT) and the \textit{Unoverloading Rule} (UO). 
 The consistency of Isabelle/HOL augmented with the LT and
 the UO is proved in Theorem 11 in \<^cite>\<open>"yang_comprehending_2017"\<close>.
 
 The LT is given by
 \[
 \begin{aligned}
 \scalebox{1.0}{
 \infer[\beta \not\in U, \phi, \Gamma]{\Gamma \vdash \phi}{%
 \Gamma\vdash U \neq\emptyset
 & \Gamma
   \vdash
   \left( 
     \exists \mathsf{Abs}\ \mathsf{Rep}. {}_{\sigma}(\beta\approx U)_{\mathsf{Rep}}^{\mathsf{Abs}}\longrightarrow\phi 
   \right)
 } 
 }
 \end{aligned}
 \]
 
 Thus, if $\beta$ is fresh for the non-empty set $U_{\sigma\ \mathsf{set}}$, 
 the formula $\phi$ and the context $\Gamma$, then $\phi$ can be proved in 
 $\Gamma$ by assuming the existence of a type $\beta$ isomorphic to $U$.
 
 The UO is given by
 \[
 \infer[\text{$\forall u$ in $\phi$}. \neg(u\rightsquigarrow^{\downarrow+}c_{\sigma});\ \sigma\not\leq\Delta_c]{\forall x_{\sigma}. \phi\left[x_{\sigma}/c_{\sigma}\right]}{\phi}
 \]
 Thus, a \textit{constant-instance} $c_{\sigma}$ may be replaced by a universally 
 quantified variable $x_{\sigma}$ in $\phi$, if all types and 
 constant-instances in $\phi$ do not semantically depend on $c_{\sigma}$ 
 through a chain of constant and type definitions and there is no 
 matching definition for $c_{\sigma}$.
 
 The statement of the \textit{original relativization algorithm} (ORA) can be 
 found in subsection 5.4 in \<^cite>\<open>"blanchette_types_2016"\<close>. Here, we present
 a variant of the algorithm that includes some of the amendments that were 
 introduced in \<^cite>\<open>"immler_smooth_2019"\<close>, which will be referred to as the 
 \textit{relativization algorithm} (RA). 
 The differences between the ORA and 
 the RA are implementation-specific and have no effect on the output 
 of the algorithm, if applied to a conventional input.
 Let $\bar{a}$ denote a finite sequence $a_1,\ldots,a_n$ 
 for some positive integer $n$; let $\Upsilon$ be a \textit{type class} 
 \<^cite>\<open>"nipkow_type_1991" and "wenzel_type_1997" and "altenkirch_constructive_2007"\<close> 
 that depends on the overloaded constants $\bar{*}$ and 
 let $U\downarrow\bar{f}$ be used 
 to state that $U$ is closed under the operations $\bar{f}$; 
 then the RA is given by 
 \[
 \infer[(7)]
 {
 \vdash ?U_{?\alpha\ \mathsf{set}} \neq\emptyset\longrightarrow
 ?U\downarrow?\bar{f}\left[?\alpha\right]\longrightarrow
 \Upsilon^{\mathsf{on}}_{\mathsf{with}}\ ?U\ ?\bar{f}\longrightarrow
 \phi^{\mathsf{on}}_{\mathsf{with}}\left[?\alpha,?U,?\bar{f}\right]
 }
 {
 \infer[(6)]
 {
 U_{\alpha\ \mathsf{set}}\neq\emptyset
 \vdash U\downarrow?\bar{f}\left[\alpha\right]\longrightarrow
 \Upsilon^{\mathsf{on}}_{\mathsf{with}}\ U\ ?\bar{f}\longrightarrow
 \phi^{\mathsf{on}}_{\mathsf{with}}\left[\alpha,U,?\bar{f}\right]
 }
 {
 \infer[(5)]
 {
 U\neq\emptyset,{}_{\alpha}(\beta\approx U)_{\mathsf{Rep}}^{\mathsf{Abs}}
 \vdash U\downarrow?\bar{f}\left[\alpha\right]\longrightarrow
 \Upsilon^{\mathsf{on}}_{\mathsf{with}}\ U\ ?\bar{f}\longrightarrow
 \phi^{\mathsf{on}}_{\mathsf{with}}\left[\alpha,U,?\bar{f}\right]
 }
 {
 \infer[(4)]
 {
 U\neq\emptyset,{}_{\alpha}(\beta\approx U)_{\mathsf{Rep}}^{\mathsf{Abs}}
 \vdash\Upsilon_{\mathsf{with}}\ ?\bar{f}\left[\beta\right]\longrightarrow
 \phi_{\mathsf{with}}\left[\beta,?\bar{f}\right]
 }
 {
 \infer[(3)]
 {
 U\neq\emptyset,{}_{\alpha}(\beta\approx U)_{\mathsf{Rep}}^{\mathsf{Abs}}
 \vdash\Upsilon_{\mathsf{with}}\ ?\bar{f}\left[?\alpha\right]\longrightarrow
 \phi_{\mathsf{with}}\left[?\alpha,?\bar{f}\right]
 }
 {
 \infer[(2)]
 {
 \vdash\Upsilon_{\mathsf{with}}\ ?\bar{f}\left[?\alpha\right]\longrightarrow
 \phi_{\mathsf{with}}\left[?\alpha,?\bar{f}\right]
 }
 {
 \infer[(1)]
 {\vdash\phi_{\mathsf{with}}\left[?\alpha_{\Upsilon},\bar{*}\right]}
 {\vdash\phi\left[?\alpha_{\Upsilon}\right]}
 }
 }
 }
 }
 }
 }
 \]
 The input to the RA is assumed to be a theorem 
 $\vdash\phi\left[?\alpha_{\Upsilon}\right]$. 
 Step 1 will be referred to as the first step of the dictionary 
 construction (subsection 5.2 in \<^cite>\<open>"blanchette_types_2016"\<close>); 
 step 2 as unoverloading of the type $?\alpha_{\Upsilon}$: 
 it includes class internalization (subsection 5.1 in \<^cite>\<open>"blanchette_types_2016"\<close>) 
 and the application of the UO (it corresponds to the application 
 of the attribute @{attribute unoverload_type} \<^cite>\<open>"immler_smooth_2019"\<close>); 
 step 3 provides the assumptions that are the prerequisites for 
 the application of the LT; 
 step 4 is reserved for the concrete type instantiation; 
 step 5 is the application of \textit{Transfer} 
 (section 6 in \<^cite>\<open>"blanchette_types_2016"\<close>); 
 step 6 refers to the application of the LT; 
 step 7 is the export of the theorem from the local 
 context \<^cite>\<open>"wenzel_isabelle/isar_2019"\<close>.
 \<close>
 
 
 subsubsection\<open>Implementation of Types-To-Sets\label{subsec:ITTS}\<close>
 
 
 text\<open>
 
 In \<^cite>\<open>"blanchette_types_2016"\<close>, the authors extended the implementation 
 of Isabelle/HOL with the LT and UO. Also, they introduced the 
 attributes @{attribute internalize_sort},
 @{attribute unoverload} and @{attribute cancel_type_definition}  
 that allowed for the execution of steps 1, 3 and 7 (respectively) of the ORA. 
 Other steps could be performed using the technology that already existed. 
 In \<^cite>\<open>"immler_smooth_2019"\<close>, the implementation was augmented with the 
 attribute @{attribute unoverload_type},
 which largely subsumed the functionality of the attributes 
 @{attribute internalize_sort} and @{attribute unoverload}.
 
 The examples of the application of the ORA to theorems in 
 Isabelle/HOL that were developed in \<^cite>\<open>"blanchette_types_2016"\<close>
 already contained an implicit suggestion that the constants and theorems 
 needed for the first step of the dictionary construction in step 2 of 
 the ORA and the \textit{transfer rules} \<^cite>\<open>"kuncar_types_2015"\<close> 
 needed for step 6 of the ORA can and should 
 be obtained prior to the application of the algorithm. Thus, using the notation
 from subsection \ref{sec:ra}, for each constant-instance $c_{\sigma}$ 
 that occurs in the type-based theorem 
 $\vdash\phi\left[?\alpha_{\Upsilon}\right]$
 prior to the application of the ORA with respect to 
 ${}_{\alpha}(\beta \approx U)_{\mathsf{Rep}}^{\mathsf{Abs}}$, 
 the users were expected to provide
 an \textit{unoverloaded} constant $c_{\mathsf{with}}$ such that 
 $c_{\sigma} = c_{\mathsf{with}}\ \bar{*}$, 
 and a \textit{relativized} constant 
 $c^{\mathsf{on}}_{\mathsf{with}}$ 
 such that $R\left[T_{\alpha\rightarrow\beta\rightarrow\mathbb{B}}\right]
 \ (c^{\mathsf{on}}_{\mathsf{with}}\ U_{\alpha\ \mathsf{set}})\ c_{\mathsf{with}}$ 
 ($\mathbb{B}$ denotes the built-in Isabelle/HOL type $bool$
 \<^cite>\<open>"kuncar_types_2015"\<close>)
 is a conditional transfer rule (e.g., see \<^cite>\<open>"gonthier_lifting_2013"\<close>), 
 with $T$ being a binary 
 relation that is at least right-total and bi-unique, 
 assuming the default order on predicates
 in Isabelle/HOL (see \<^cite>\<open>"kuncar_types_2015"\<close>).  
 
 The unoverloading \<^cite>\<open>"kaufmann_mechanized_2010"\<close> 
 and relativization of constants for the application 
 of the RA was performed manually in 
 \<^cite>\<open>"blanchette_types_2016" and "kuncar_types_2019" and "immler_smooth_2019"\<close>. 
 Nonetheless, unoverloading could be performed using the 
 \textit{classical overloading elimination algorithm} proposed 
 in \<^cite>\<open>"kaufmann_mechanized_2010"\<close>, but it is likely that an implementation
 of this algorithm was not publicly available at the time of writing
 of this document. In \<^cite>\<open>"immler_automation_2019"\<close>, an alternative algorithm was 
 implemented and made available via the command 
 @{command unoverload_definition}, 
 although it suffers from several limitations in comparison to the 
 algorithm in \<^cite>\<open>"kaufmann_mechanized_2010"\<close>. 
 The transfer rules 
 for the constants that are conditionally parametric 
 can be synthesized automatically using the command 
 @{command parametric_constant} 
 \<^cite>\<open>"gilcher_conditional_2017"\<close> from the standard distribution of Isabelle; 
 the framework \textit{autoref} \<^cite>\<open>"lammich_automatic_2013"\<close> allows 
 for the synthesis of transfer rules $R\ t\ t'$, 
 including both the \textit{parametricity relation} \<^cite>\<open>"kuncar_types_2015"\<close>
 $R$ and the term $t$, 
 based on $t'$, under favorable conditions; 
 lastly, in \<^cite>\<open>"lammich_automatic_2013"\<close> and \<^cite>\<open>"immler_smooth_2019"\<close>, 
 the authors suggest an outline of another feasible algorithm for the 
 synthesis of the transfer rules based on the functionality of the framework
 Transfer \<^cite>\<open>"gonthier_lifting_2013"\<close>, but do not provide an implementation.
 
 Finally, the assumption 
 ${}_{\alpha}(\beta \approx U)_{\mathsf{Rep}}^{\mathsf{Abs}}$ 
 can be stated using the constant @{const type_definition}
 from the standard library of Isabelle/HOL as 
 \<^term>\<open>type_definition Rep Abs U\<close>;
 the instantiation of types required in step 4 of the RA can 
 be performed using the standard attributes of Isabelle; 
 step 6 can be performed using the attribute 
 @{attribute cancel_type_definition} developed in 
 \<^cite>\<open>"blanchette_types_2016"\<close>; step 7 is expected to be performed manually
 by the user.
 
 \<close>
 
 
 
 subsection\<open>Purpose and scope\<close>
 
 
 text\<open>
 The extension of the framework Types-To-Sets that is described in this manual
 adds a further layer of automation to the existing implementation
 of the framework Types-To-Sets. The primary functionality of the extension 
 is available via the following Isar commands: 
 @{command tts_context}, @{command tts_lemmas} and @{command tts_lemma} (and the
 synonymous commands @{command tts_corollary}, @{command tts_proposition} and
 @{command tts_theorem}\footnote{In what follows, any reference to the 
 command @{command tts_lemma} should be viewed as a reference to the 
 entire family of the commands with the identical functionality.}).
 The commands @{command tts_lemmas} and @{command tts_lemma}, when invoked inside
 an appropriately defined @{command tts_context} provide the 
 functionality that is approximately equivalent to the application of all 
 steps of the RA and several additional steps of 
 pre-processing of the input and post-processing of the result
 (collectively referred to as the \textit{extended relativization algorithm} 
-or ERA). 
+or ERA).
 
 As part of our work on the ETTS, we have also designed 
 the auxiliary framework \textit{Conditional Transfer Rule} (CTR). 
 The framework CTR provides the commands @{command ud} and @{command ctr} for
 the automation of unoverloading of definitions and 
 synthesis of conditional transfer rules from definitions, 
 respectively. Further information about this framework can be found in its
 reference manual \<^cite>\<open>"milehins_conditional_2021"\<close>.
 In this context, we also mention that both the CTR and the ETTS were tested 
-using the framework SpecCheck \<^cite>\<open>"kappelmann_speccheck_2021"\<close>.
+using the framework SpecCheck \<^cite>\<open>"kappelmann_speccheck_2021"\<close>.\footnote{
+Some of the elements of the content of the tests are based on the 
+elements of the content of \<^cite>\<open>"cain_nine_2019"\<close>.}
 
 The extension was designed under a policy of non-intervention with the  
 existing implementation of the framework Types-To-Sets. Therefore, it does
 not reduce the scope of the applicability of the framework. 
 However, the functionality that is provided by the commands associated with the 
 extension is a proper subset of the functionality provided by the existing 
 implementation. Nevertheless, the author of the extension believes that there 
 exist very few practical applications of the relativization algorithm that 
 can be solved using the original interface but cannot be solved using 
 the commands that are introduced within the scope of the 
 extension.
 
 \<close>
 
 text\<open>\newpage\<close>
 
 end
\ No newline at end of file
diff --git a/thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_Tests.thy b/thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_Tests.thy
--- a/thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_Tests.thy
+++ b/thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_Tests.thy
@@ -1,365 +1,365 @@
 (* Title: ETTS/Tests/ETTS_Tests.thy
    Author: Mihails Milehins
    Copyright 2021 (C) Mihails Milehins
 
 A test suite for the ETTS.
 *)
 
 section\<open>A test suite for ETTS\<close>
 theory ETTS_Tests
   imports
     "../ETTS_Auxiliary"
     Conditional_Transfer_Rule.IML_UT
 begin
 
 
 
 subsection\<open>\<open>amend_ctxt_data\<close>\<close>
 
 ML_file\<open>ETTS_TEST_AMEND_CTXT_DATA.ML\<close>
 
 locale test_amend_ctxt_data =
   fixes UA :: "'ao set" and UB :: "'bo set" and UC :: "'co set"
     and le :: "['ao, 'ao] \<Rightarrow> bool" (infix \<open>\<le>\<^sub>o\<^sub>w\<close> 50) 
     and ls :: "['bo, 'bo] \<Rightarrow> bool" (infix \<open><\<^sub>o\<^sub>w\<close> 50)
     and f :: "['ao, 'bo] \<Rightarrow> 'co"
   assumes closed_f: "\<lbrakk> a \<in> UA; b \<in> UB \<rbrakk> \<Longrightarrow> f a b \<in> UC"
 begin
 
 notation le (\<open>'(\<le>\<^sub>o\<^sub>w')\<close>)
   and le (infix \<open>\<le>\<^sub>o\<^sub>w\<close> 50) 
   and ls (\<open>'(<\<^sub>o\<^sub>w')\<close>) 
   and ls (infix \<open><\<^sub>o\<^sub>w\<close> 50)
 
 tts_register_sbts \<open>(\<le>\<^sub>o\<^sub>w)\<close> | UA
 proof-
   assume "Domainp AOA = (\<lambda>x. x \<in> UA)" "bi_unique AOA" "right_total AOA" 
   from tts_AA_eq_transfer[OF this] show ?thesis by auto
 qed
 
 tts_register_sbts \<open>(<\<^sub>o\<^sub>w)\<close> | UB
 proof-
   assume "Domainp BOA = (\<lambda>x. x \<in> UB)" "bi_unique BOA" "right_total BOA"
   from tts_AA_eq_transfer[OF this] show ?thesis by auto
 qed
 
 tts_register_sbts f | UA and UB and UC
 proof-
   assume 
     "Domainp AOC = (\<lambda>x. x \<in> UA)" "bi_unique AOC" "right_total AOC"
     "Domainp BOB = (\<lambda>x. x \<in> UB)" "bi_unique BOB" "right_total BOB"
     "Domainp COA = (\<lambda>x. x \<in> UC)" "bi_unique COA" "right_total COA"
   from tts_AB_C_transfer[OF closed_f this] show ?thesis by auto
 qed
 
 end
 
 context test_amend_ctxt_data
 begin
 ML\<open>
 Lecker.test_group @{context} () [etts_test_amend_ctxt_data.test_suite]
 \<close>
 end
 
 
 
 subsection\<open>\<open>tts_algorithm\<close>\<close>
 
 
 text\<open>
 Some of the elements of the content of this section are based on the 
-elements of the content of \cite{cain_nine_2019}. 
+elements of the content of \<^cite>\<open>"cain_nine_2019"\<close>. 
 \<close>
 
 (*the following theorem is restated for forward compatibility*)
 lemma exI': "P x \<Longrightarrow> \<exists>x. P x" by auto
 
 class tta_mult =
   fixes tta_mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*\<^sub>t\<^sub>t\<^sub>a" 65)
 
 class tta_semigroup = tta_mult +
   assumes tta_assoc[simp]: "(a *\<^sub>t\<^sub>t\<^sub>a b) *\<^sub>t\<^sub>t\<^sub>a c = a *\<^sub>t\<^sub>t\<^sub>a (b *\<^sub>t\<^sub>t\<^sub>a c)"
 
 definition set_mult :: "'a::tta_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "\<^bold>*\<^sub>t\<^sub>t\<^sub>a" 65) 
   where "set_mult S T = {s *\<^sub>t\<^sub>t\<^sub>a t | s t. s \<in> S \<and> t \<in> T}"
 
 definition left_ideal :: "'a::tta_mult set \<Rightarrow> bool"
   where "left_ideal T \<longleftrightarrow> (\<forall>s. \<forall>t\<in>T. s *\<^sub>t\<^sub>t\<^sub>a t \<in> T)"
 
 lemma left_idealI[intro]:
   assumes "\<And>s t. t \<in> T \<Longrightarrow> s *\<^sub>t\<^sub>t\<^sub>a t \<in> T"
   shows "left_ideal T"
   using assms unfolding left_ideal_def by simp
 
 lemma left_idealE[elim]:
   assumes "left_ideal T"
   obtains "\<And>s t. t \<in> T \<Longrightarrow> s *\<^sub>t\<^sub>t\<^sub>a t \<in> T"
   using assms unfolding left_ideal_def by simp
 
 lemma left_ideal_set_mult_iff: "left_ideal T \<longleftrightarrow> UNIV \<^bold>*\<^sub>t\<^sub>t\<^sub>a T \<subseteq> T"
   unfolding left_ideal_def set_mult_def by auto
 
 ud \<open>set_mult\<close> 
 ud \<open>left_ideal\<close>
 
 ctr relativization
   synthesis ctr_simps
   assumes [transfer_domain_rule]: "Domainp A = (\<lambda>x. x \<in> U)"
     and [transfer_rule]: "bi_unique A" "right_total A" 
   trp (?'a A)
   in set_mult_ow: set_mult.with_def 
     and left_ideal_ow: left_ideal.with_def 
 
 locale tta_semigroup_hom =
   fixes f :: "'a::tta_semigroup \<Rightarrow> 'b::tta_semigroup"
   assumes hom: "f (a *\<^sub>t\<^sub>t\<^sub>a b) = f a *\<^sub>t\<^sub>t\<^sub>a f b"
 
 context tta_semigroup_hom
 begin
 
 lemma tta_left_ideal_closed:
   assumes "left_ideal T" and "surj f"
   shows "left_ideal (f ` T)"
   unfolding left_ideal_def
 proof(intro allI ballI)
   fix fs ft assume prems: "ft \<in> f ` T"
   then obtain t where t: "t \<in> T" and ft_def: "ft = f t" by clarsimp
   from assms(2) obtain s where fs_def: "fs = f s" by auto
   from assms have "t \<in> T \<Longrightarrow> s *\<^sub>t\<^sub>t\<^sub>a t \<in> T" for s t by auto
   with t show "fs *\<^sub>t\<^sub>t\<^sub>a ft \<in> f ` T" 
     unfolding ft_def fs_def hom[symmetric] by simp
 qed
 
 end
 
 locale semigroup_mult_hom_with = 
   dom: tta_semigroup times_a + cod: tta_semigroup times_b
   for times_a (infixl \<open>*\<^sub>o\<^sub>w\<^sub>.\<^sub>a\<close> 70) and times_b (infixl \<open>*\<^sub>o\<^sub>w\<^sub>.\<^sub>b\<close> 70) +
   fixes f :: "'a \<Rightarrow> 'b"
   assumes f_hom: "f (a *\<^sub>o\<^sub>w\<^sub>.\<^sub>a b) = f a *\<^sub>o\<^sub>w\<^sub>.\<^sub>b f b"
 
 lemma semigroup_mult_hom_with[ud_with]:
   "tta_semigroup_hom = semigroup_mult_hom_with (*\<^sub>t\<^sub>t\<^sub>a) (*\<^sub>t\<^sub>t\<^sub>a)"
   unfolding 
     semigroup_mult_hom_with_def tta_semigroup_hom_def 
     class.tta_semigroup_def semigroup_mult_hom_with_axioms_def
   by auto
 
 locale semigroup_ow = 
   fixes U :: "'ag set" and f :: "['ag, 'ag] \<Rightarrow> 'ag" (infixl \<open>\<^bold>*\<^sub>o\<^sub>w\<close> 70)
   assumes f_closed: "\<lbrakk> a \<in> U; b \<in> U \<rbrakk> \<Longrightarrow> a \<^bold>*\<^sub>o\<^sub>w b \<in> U"
     and assoc: "\<lbrakk> a \<in> U; b \<in> U; c \<in> U \<rbrakk> \<Longrightarrow> a \<^bold>*\<^sub>o\<^sub>w b \<^bold>*\<^sub>o\<^sub>w c = a \<^bold>*\<^sub>o\<^sub>w (b \<^bold>*\<^sub>o\<^sub>w c)"
 begin
 
 notation f (infixl \<open>\<^bold>*\<^sub>o\<^sub>w\<close> 70)
 
 lemma f_closed'[simp]: "\<forall>x\<in>U. \<forall>y\<in>U. x \<^bold>*\<^sub>o\<^sub>w y \<in> U" by (simp add: f_closed)
 
 tts_register_sbts \<open>(\<^bold>*\<^sub>o\<^sub>w)\<close> | U by (rule tts_AA_A_transfer[OF f_closed])
 
 end
 
 locale times_ow =
   fixes U :: "'ag set" and times :: "['ag, 'ag] \<Rightarrow> 'ag" (infixl \<open>*\<^sub>o\<^sub>w\<close> 70)
   assumes times_closed[simp, intro]: "\<lbrakk> a \<in> U; b \<in> U \<rbrakk> \<Longrightarrow> a *\<^sub>o\<^sub>w b \<in> U"
 begin
 
 notation times (infixl \<open>*\<^sub>o\<^sub>w\<close> 70)
 
 lemma times_closed'[simp]: "\<forall>x\<in>U. \<forall>y\<in>U. x *\<^sub>o\<^sub>w y \<in> U" by simp
 
 tts_register_sbts \<open>(*\<^sub>o\<^sub>w)\<close> | U  by (rule tts_AA_A_transfer[OF times_closed])
 
 end
 
 locale semigroup_mult_ow = times_ow U times 
   for U :: "'ag set" and times +
   assumes mult_assoc: 
     "\<lbrakk> a \<in> U; b \<in> U; c \<in> U \<rbrakk> \<Longrightarrow> a *\<^sub>o\<^sub>w b *\<^sub>o\<^sub>w c = a *\<^sub>o\<^sub>w (b *\<^sub>o\<^sub>w c)"
 begin
 
 sublocale mult: semigroup_ow U \<open>(*\<^sub>o\<^sub>w)\<close> 
   by unfold_locales (auto simp: times_closed' mult_assoc)
 
 end
 
 locale semigroup_mult_hom_ow = 
   dom: semigroup_mult_ow UA times_a + 
   cod: semigroup_mult_ow UB times_b 
   for UA :: "'a set" 
     and UB :: "'b set" 
     and times_a (infixl \<open>*\<^sub>o\<^sub>w\<^sub>.\<^sub>a\<close> 70) 
     and times_b (infixl \<open>*\<^sub>o\<^sub>w\<^sub>.\<^sub>b\<close> 70) +
   fixes f :: "'a \<Rightarrow> 'b"
   assumes f_closed[simp]: "a \<in> UA \<Longrightarrow> f a \<in> UB"
     and f_hom: "\<lbrakk> a \<in> UA; b \<in> UA \<rbrakk> \<Longrightarrow> f (a *\<^sub>o\<^sub>w\<^sub>.\<^sub>a b) = f a *\<^sub>o\<^sub>w\<^sub>.\<^sub>b f b"
 begin
 
 lemma f_closed'[simp]: "f ` UA \<subseteq> UB" by auto
 
 tts_register_sbts f | UA and UB by (rule tts_AB_transfer[OF f_closed'])
 
 end
 
 context semigroup_mult_hom_ow
 begin
 
 lemma tta_left_ideal_ow_closed:
   assumes "T \<subseteq> UA"
     and "left_ideal_ow UA (*\<^sub>o\<^sub>w\<^sub>.\<^sub>a) T"
     and "f ` UA = UB"
   shows "left_ideal_ow UB (*\<^sub>o\<^sub>w\<^sub>.\<^sub>b) (f ` T)"
   unfolding left_ideal_ow_def
 proof(intro ballI)
   fix fs ft assume ft: "ft \<in> f ` T" and fs: "fs \<in> UB"
   then obtain t where t: "t \<in> T" and ft_def: "ft = f t" by auto
   from assms(3) fs obtain s where fs_def: "fs = f s" and s: "s \<in> UA" by auto
   from assms have "\<lbrakk> s \<in> UA; t \<in> T \<rbrakk> \<Longrightarrow> s *\<^sub>o\<^sub>w\<^sub>.\<^sub>a t \<in> T" for s t 
     unfolding left_ideal_ow_def by simp
   with assms(1) s t fs show "fs *\<^sub>o\<^sub>w\<^sub>.\<^sub>b ft \<in> f ` T" 
     using f_hom[symmetric, OF s] unfolding ft_def fs_def by auto
 qed
 
 end
 
 lemma semigroup_mult_ow: "class.tta_semigroup = semigroup_mult_ow UNIV"
   unfolding 
     class.tta_semigroup_def semigroup_mult_ow_def
     semigroup_mult_ow_axioms_def times_ow_def
   by simp
 
 lemma semigroup_mult_hom_ow: 
   "tta_semigroup_hom = semigroup_mult_hom_ow UNIV UNIV (*\<^sub>t\<^sub>t\<^sub>a) (*\<^sub>t\<^sub>t\<^sub>a)"
   unfolding 
     tta_semigroup_hom_def semigroup_mult_hom_ow_axioms_def
     semigroup_mult_hom_ow_def semigroup_mult_ow_def 
     semigroup_mult_ow_axioms_def times_ow_def
   by simp
 
 context
   includes lifting_syntax
 begin
 
 lemma semigroup_transfer[transfer_rule]:
   assumes [transfer_rule]: "bi_unique A" "right_total A" 
   shows 
     "((A ===> A ===> A) ===> (=))
       (semigroup_ow (Collect (Domainp A))) semigroup"
 proof-
   let ?P = "((A ===> A ===> A) ===> (=))"
   let ?semigroup_ow = "semigroup_ow (Collect (Domainp A))"
   let ?rf_UNIV = 
     "(\<lambda>f::['b, 'b] \<Rightarrow> 'b. (\<forall>x y. x \<in> UNIV \<longrightarrow> y \<in> UNIV \<longrightarrow> f x y \<in> UNIV))"
   have "?P ?semigroup_ow (\<lambda>f. ?rf_UNIV f \<and> semigroup f)"
     unfolding semigroup_ow_def semigroup_def
     apply transfer_prover_start
     apply transfer_step+
     by simp
   thus ?thesis by simp
 qed
 
 lemma semigroup_mult_transfer[transfer_rule]:
   assumes [transfer_rule]: "bi_unique A" "right_total A" 
   shows
     "((A ===> A ===> A) ===> (=))
       (semigroup_mult_ow (Collect (Domainp A)))
       class.tta_semigroup"
 proof -
   let ?P = \<open>((A ===> A ===> A) ===> (=))\<close>
     and ?semigroup_mult_ow = 
       \<open>(\<lambda>f. semigroup_mult_ow (Collect (Domainp A)) f)\<close>
     and ?rf_UNIV = 
       \<open>(\<lambda>f::['b, 'b] \<Rightarrow> 'b. (\<forall>x y. x \<in> UNIV \<longrightarrow> y \<in> UNIV \<longrightarrow> f x y \<in> UNIV))\<close>
   have "?P ?semigroup_mult_ow (\<lambda>f. ?rf_UNIV f \<and> class.tta_semigroup f)"
     unfolding 
       semigroup_mult_ow_def class.tta_semigroup_def
       semigroup_mult_ow_axioms_def times_ow_def
     apply transfer_prover_start
     apply transfer_step+
     by simp
   thus ?thesis by simp
 qed
 
 lemma semigroup_mult_hom_transfer[transfer_rule]:
   assumes [transfer_rule]: 
     "bi_unique A" "right_total A" "bi_unique B" "right_total B" 
   shows
     "((A ===> A ===> A) ===> (B ===> B ===> B) ===> (A ===> B) ===> (=))
       (semigroup_mult_hom_ow (Collect (Domainp A)) (Collect (Domainp B)))
       semigroup_mult_hom_with"
 proof-
   let ?PA = "A ===> A ===> A"
     and ?PB = "B ===> B ===> B"
     and ?semigroup_mult_hom_ow = 
       \<open>
         \<lambda>times_a times_b f. semigroup_mult_hom_ow 
           (Collect (Domainp A)) (Collect (Domainp B)) times_a times_b f
       \<close>
   let ?closed = \<open>\<lambda>f::'b\<Rightarrow>'d . \<forall>a. a \<in> UNIV \<longrightarrow> f a \<in> UNIV\<close>
   have
     "(?PA ===> ?PB ===> (A ===> B) ===> (=))
       ?semigroup_mult_hom_ow
       (
         \<lambda>times_a times_b f. 
           ?closed f \<and> semigroup_mult_hom_with times_a times_b f
       )"
     unfolding 
       times_ow_def
       semigroup_mult_hom_ow_def 
       semigroup_mult_hom_ow_axioms_def 
       semigroup_mult_hom_with_def
       semigroup_mult_hom_with_axioms_def
     apply transfer_prover_start
     apply transfer_step+
     by blast
   thus ?thesis by simp
 qed
 
 end
 
 
 context semigroup_mult_hom_ow
 begin
 
 ML_file\<open>ETTS_TEST_TTS_ALGORITHM.ML\<close>
 
 named_theorems semigroup_mult_hom_ow_test_simps
 
 lemmas [semigroup_mult_hom_ow_test_simps] = 
   ctr_simps_Collect_mem_eq
   ctr_simps_in_iff
 
 tts_context
   tts: (?'a to UA) and (?'b to UB)
   sbterms: (\<open>(*\<^sub>t\<^sub>t\<^sub>a)::[?'a::tta_semigroup, ?'a] \<Rightarrow> ?'a\<close> to \<open>(*\<^sub>o\<^sub>w\<^sub>.\<^sub>a)\<close>)
     and (\<open>(*\<^sub>t\<^sub>t\<^sub>a)::[?'b::tta_semigroup, ?'b] \<Rightarrow> ?'b\<close> to \<open>(*\<^sub>o\<^sub>w\<^sub>.\<^sub>b)\<close>)
     and (\<open>?f::?'a::tta_semigroup \<Rightarrow> ?'b::tta_semigroup\<close> to f)
   rewriting semigroup_mult_hom_ow_test_simps
   substituting semigroup_mult_hom_ow_axioms
     and dom.semigroup_mult_ow_axioms
     and cod.semigroup_mult_ow_axioms
   eliminating \<open>UA \<noteq> {}\<close> and \<open>UB \<noteq> {}\<close> 
     through (auto simp only: left_ideal_ow_def)
 begin
 ML\<open>
 Lecker.test_group @{context} () [etts_test_tts_algorithm.test_suite]
 \<close>
 end
 
 end
 
 
 
 subsection\<open>\<open>tts_register_sbts\<close>\<close>
 
 context
   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
     and UA :: "'a set"
 begin
 ML_file\<open>ETTS_TEST_TTS_REGISTER_SBTS.ML\<close>
 ML\<open>
 Lecker.test_group @{context} () [etts_test_tts_register_sbts.test_suite]
 \<close>
 end
 
 end
\ No newline at end of file
diff --git a/thys/Types_To_Sets_Extension/document/root.bib b/thys/Types_To_Sets_Extension/document/root.bib
--- a/thys/Types_To_Sets_Extension/document/root.bib
+++ b/thys/Types_To_Sets_Extension/document/root.bib
@@ -1,308 +1,314 @@
 @incollection{blanchette_types_2016,
 	address = {Heidelberg},
 	title = {From {Types} to {Sets} by {Local} {Type} {Definitions} in {Higher}-{Order} {Logic}},
 	volume = {9807},
 	isbn = {978-3-319-43144-4},
 	booktitle = {Interactive {Theorem} {Proving}},
 	publisher = {Springer},
 	author = {Kun{\v c}ar, Ond{\v r}ej and Popescu, Andrei},
 	editor = {Blanchette, Jasmin Christian and Merz, Stephan},
 	year = {2016},
 	pages = {200--218},
 }
 @book{urban_isabelle_2019,
 	title = {The {Isabelle} {Cookbook}: {A} {Gentle} {Tutorial} for {Programming} {Isabelle}/{ML}},
 	author = {Urban, Christian},
 	collaborator = {Berghofer, Stefan and Blanchette, Jasmin and Bohme, Sascha and Bulwahn, Lukas and Dawson, Jeremy and Kolanski, Rafal and Krauss, Alexander and Nipkow, Tobias and Schropp, Andreas and Sternagel, Christian},
 	year = {2019},
 }
 @incollection{immler_smooth_2019,
 	address = {New York},
 	series = {{CPP} 2019},
 	title = {Smooth {Manifolds} and {Types} to {Sets} for {Linear} {Algebra} in {Isabelle}/{HOL}},
 	isbn = {978-1-4503-6222-1},
 	booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} {International} {Conference} on {Certified} {Programs} and {Proofs}, {CPP} 2019, {Cascais}, {Portugal}},
 	publisher = {ACM},
 	author = {Immler, Fabian and Zhan, Bohua},
 	editor = {Mahboubi, Assia and Myreen, Magnus O.},
 	year = {2019},
 	keywords = {Formalization of Mathematics, Higher Order Logic, Isabelle, Manifolds},
 	pages = {65--77},
 }
 @misc{immler_automation_2019,
 	title = {Automation for unverloading definitions},
 	url = {http://isabelle.in.tum.de/repos/isabelle/rev/ab5a8a2519b0},
 	journal = {isabelle/changeset},
 	author = {Immler, Fabian},
 	year = {2019},
 }
 @phdthesis{kuncar_types_2015,
 	address = {Munich},
 	title = {Types, {Abstraction} and {Parametric} {Polymorphism} in {Higher}-{Order} {Logic}},
 	school = {Technische Universit{\"a}t M{\"u}nchen},
 	author = {Kun{\v c}ar, Ond{\v r}ej},
 	year = {2015},
 }
 @unpublished{wenzel_isabelle/isar_2019,
 	title = {The {Isabelle}/{Isar} {Implementation}},
 	author = {Wenzel, Makarius},
 	collaborator = {Berghofer, Stefan and Haftmann, Florian and Paulson, Larry},
 	year = {2019},
 }
 @unpublished{wenzel_isabelle/isar_2019-1,
 	title = {The {Isabelle}/{Isar} {Reference} {Manual}},
 	author = {Wenzel, Makarius},
 	collaborator = {Ballarin, Clemens and Berghofer, Stefan and Blanchette, Jasmin and Bourke, Timothy and Bulwahn, Lukas and Chaieb, Amine and Dixon, Lucas and Haftmann, Florian and Huffman, Brian and Hupel, Lars and Klein, Gerwin and Krauss, Alexander and Kun{\v c}ar, Ond{\v r}ej and Lochbihler, Andreas and Nipkow, Tobias and Noschinski, Lars and Oheimb, David von and Paulson, Larry and Skalberg, Sebastian and Sternagel, Christian and Traytel, Dmitriy},
 	year = {2019},
 }
 @phdthesis{wenzel_isabelle/isar_2001,
 	address = {Munich},
 	title = {Isabelle/{Isar} {\textemdash} {A} {Versatile} {Environment} for {Human}-{Readable} {Formal} {Proof} {Documents}},
 	school = {Technische Universit{\"a}t M{\"u}nchen},
 	author = {Wenzel, Markus M.},
 	year = {2001},
 }
 @inproceedings{gilcher_conditional_2017,
 	address = {Bras{\'i}lia, Brazil},
 	title = {Conditional {Parametricity} in {Isabelle}/{HOL}},
 	booktitle = {{TABLEAUX}/{FroCoS}/{ITP}},
 	author = {Gilcher, Jan and Lochbihler, Andreas and Traytel, Dmitriy},
 	year = {2017},
 }
 @article{divason_perron-frobenius_2016,
 	title = {Perron-{Frobenius} {Theorem} for {Spectral} {Radius} {Analysis}},
 	journal = {Archive of Formal Proofs},
 	author = {Divas{\'o}n, Jose and Kun{\v c}ar, Ond{\v r}ej and Thiemann, Ren{\'e} and Yamada, Akihisa},
 	year = {2016},
 }
 @article{maletzky_hilberts_2019,
 	title = {Hilbert's {Nullstellensatz}},
 	journal = {Archive of Formal Proofs},
 	author = {Maletzky, Alexander},
 	year = {2019},
 }
 @incollection{berardi_locales_2004,
 	address = {Heidelberg},
 	title = {Locales and {Locale} {Expressions} in {Isabelle}/{Isar}},
 	volume = {3085},
 	isbn = {978-3-540-22164-7},
 	booktitle = {Types for {Proofs} and {Programs}},
 	publisher = {Springer},
 	author = {Ballarin, Clemens},
 	editor = {Berardi, Stefano and Coppo, Mario and Damiani, Ferruccio},
 	year = {2004},
 	pages = {34--50},
 }
 @book{ballarin_isabellehol_2020,
 	title = {The {Isabelle}/{HOL} {Algebra} {Library}},
 	url = {https://isabelle.in.tum.de/website-Isabelle2020/dist/library/HOL/HOL-Algebra/document.pdf},
 	editor = {Ballarin, Clemens},
 	year = {2020},
 }
 @misc{noauthor_isabellehol_2020,
 	title = {Isabelle/{HOL} {Standard} {Library}},
 	url = {https://isabelle.in.tum.de/website-Isabelle2020/dist/library/HOL/HOL/index.html},
 	journal = {Isabelle/HOL},
 	year = {2020},
 }
 @misc{noauthor_isabellehol_2020-1,
 	title = {Isabelle/{HOL} {Analysis}},
 	url = {https://isabelle.in.tum.de/website-Isabelle2020/dist/library/HOL/HOL-Analysis/index.html},
 	journal = {Isabelle/HOL},
 	year = {2020},
 }
 @incollection{gonthier_lifting_2013,
 	address = {Heidelberg},
 	title = {Lifting and {Transfer}: {A} {Modular} {Design} for {Quotients} in {Isabelle}/{HOL}},
 	volume = {8307},
 	isbn = {978-3-319-03545-1},
 	booktitle = {Certified {Programs} and {Proofs}},
 	publisher = {Springer},
 	author = {Huffman, Brian and Kun{\v c}ar, Ond{\v r}ej},
 	editor = {Gonthier, Georges and Norrish, Michael},
 	year = {2013},
 	pages = {131--146},
 }
 @incollection{altenkirch_constructive_2007,
 	address = {Heidelberg},
 	title = {Constructive {Type} {Classes} in {Isabelle}},
 	volume = {4502},
 	isbn = {978-3-540-74464-1},
 	booktitle = {Types for {Proofs} and {Programs}},
 	publisher = {Springer},
 	author = {Haftmann, Florian and Wenzel, Makarius},
 	editor = {Altenkirch, Thorsten and McBride, Conor},
 	year = {2007},
 	pages = {160--174},
 }
 @article{ballarin_locales_2014,
 	title = {Locales: {A} {Module} {System} for {Mathematical} {Theories}},
 	volume = {52},
 	number = {2},
 	journal = {Journal of Automated Reasoning},
 	author = {Ballarin, Clemens},
 	year = {2014},
 	pages = {123--153},
 }
 @incollection{kaufmann_mechanized_2010,
 	address = {Heidelberg},
 	title = {A {Mechanized} {Translation} from {Higher}-{Order} {Logic} to {Set} {Theory}},
 	volume = {6172},
 	isbn = {978-3-642-14051-8},
 	booktitle = {Interactive {Theorem} {Proving}},
 	publisher = {Springer},
 	author = {Krauss, Alexander and Schropp, Andreas},
 	editor = {Kaufmann, Matt and Paulson, Lawrence C.},
 	year = {2010},
 	pages = {323--338},
 }
 @article{paulson_natural_1986,
 	title = {Natural {Deduction} as {Higher}-{Order} {Resolution}},
 	volume = {3},
 	number = {3},
 	journal = {The Journal of Logic Programming},
 	author = {Paulson, Lawrence C.},
 	year = {1986},
 	pages = {237--258},
 }
 @incollection{yang_comprehending_2017,
 	address = {Heidelberg},
 	title = {Comprehending {Isabelle}/{HOL}{\textquoteright}s {Consistency}},
 	volume = {10201},
 	isbn = {978-3-662-54433-4},
 	booktitle = {Programming {Languages} and {Systems}},
 	publisher = {Springer},
 	author = {Kun{\v c}ar, Ond{\v r}ej and Popescu, Andrei},
 	editor = {Yang, Hongseok},
 	year = {2017},
 	pages = {724--749},
 }
 @incollection{bertot_isar_1999,
 	address = {Heidelberg},
 	title = {Isar {\textemdash} {A} {Generic} {Interpretative} {Approach} to {Readable} {Formal} {Proof} {Documents}},
 	volume = {1690},
 	isbn = {978-3-540-66463-5},
 	booktitle = {Theorem {Proving} in {Higher} {Order} {Logics}},
 	publisher = {Springer},
 	author = {Wenzel, Markus},
 	editor = {Bertot, Yves and Dowek, Gilles and Th{\'e}ry, Laurent and Hirschowitz, Andr{\'e} and Paulin-Mohring, Christine},
 	year = {1999},
 	pages = {167--183},
 }
 @article{wenzel_isabelleisar_2007,
 	title = {Isabelle/{Isar} {\textemdash} a {Generic} {Framework} for {Human}-{Readable} {Proof} {Documents}},
 	volume = {10},
 	number = {23},
 	journal = {Studies in Logic, Grammar and Rhetoric},
 	author = {Wenzel, Makarius},
 	year = {2007},
 	pages = {277--297},
 }
 @incollection{kauers_context_2007,
 	address = {Heidelberg},
 	title = {Context {Aware} {Calculation} and {Deduction}: {Ring} {Equalities} {Via} {Gr{\"o}bner} {Bases} in {Isabelle}},
 	volume = {4573},
 	isbn = {978-3-540-73083-5},
 	booktitle = {Towards {Mechanized} {Mathematical} {Assistants}},
 	publisher = {Springer},
 	author = {Chaieb, Amine and Wenzel, Makarius},
 	editor = {Kauers, Manuel and Kerber, Manfred and Miner, Robert and Windsteiger, Wolfgang},
 	year = {2007},
 	pages = {27--39},
 }
 @inproceedings{lammich_automatic_2013,
 	address = {Heidelberg},
 	title = {Automatic {Data} {Refinement}},
 	isbn = {978-3-642-39634-2},
 	booktitle = {Interactive {Theorem} {Proving}},
 	publisher = {Springer},
 	author = {Lammich, Peter},
 	editor = {Blazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David},
 	year = {2013},
 	keywords = {Automatic Data, Executable Code, Side Condition, Synthesis Problem, Type Constructor},
 	pages = {84--99},
 }
 @article{kuncar_types_2019,
 	title = {From {Types} to {Sets} by {Local} {Type} {Definition} in {Higher}-{Order} {Logic}},
 	volume = {62},
 	number = {2},
 	journal = {Journal of Automated Reasoning},
 	author = {Kun{\v c}ar, Ond{\v r}ej and Popescu, Andrei},
 	year = {2019},
 	pages = {237--260},
 }
 @article{paulson_foundation_1989,
 	title = {The {Foundation} of a {Generic} {Theorem} {Prover}},
 	volume = {5},
 	number = {3},
 	journal = {Journal of Automated Reasoning},
 	author = {Paulson, Lawrence C.},
 	year = {1989},
 	pages = {363--397},
 }
 @book{milner_definition_1997,
 	address = {Cambridge, Massachusetts},
 	title = {The {Definition} of {Standard} {ML} (revised)},
 	isbn = {978-0-262-63181-5},
 	publisher = {MIT Press},
 	author = {Milner, Robin and Tofte, Mads and Harper, Robert and MacQueen, David},
 	year = {1997},
 	keywords = {ML (Computer program language)},
 }
 @inproceedings{kammuller_locales_1999,
 	address = {Heidelberg},
 	series = {Lecture {Notes} in {Computer} {Science}},
 	title = {Locales {A} {Sectioning} {Concept} for {Isabelle}},
 	isbn = {978-3-540-48256-7},
 	booktitle = {Theorem {Proving} in {Higher} {Order} {Logics}},
 	publisher = {Springer},
 	author = {Kamm{\"u}ller, Florian and Wenzel, Markus and Paulson, Lawrence C.},
 	editor = {Bertot, Yves and Dowek, Gilles and Th{\'e}ry, Laurent and Hirschowitz, Andr{\'e} and Paulin-Mohring, Christine},
 	year = {1999},
 	pages = {149--165},
 }
 @misc{immler_re_2019,
 	title = {Re: [isabelle] {Several} questions in relation to a use case for "types to sets"},
 	url = {https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-January/msg00072.html},
 	journal = {The Cl-isabelle-users Archives},
 	author = {Immler, Fabian},
 	year = {2019},
 }
 @incollection{wenzel_type_1997,
 	address = {Heidelberg},
 	series = {Lecture {Notes} in {Computer} {Science}},
 	title = {Type {Classes} and {Overloading} in {Higher}-{Order} {Logic}},
 	isbn = {978-3-540-69526-4},
 	booktitle = {Theorem {Proving} in {Higher} {Order} {Logics}},
 	publisher = {Springer},
 	author = {Wenzel, Markus},
 	editor = {Gunter, Elsa L. and Felty, Amy P.},
 	year = {1997},
 	keywords = {Type Constructor, Class Definition, Deductive System, Type Class, Type Definition},
 	pages = {307--322},
 }
 @incollection{nipkow_type_1991,
 	address = {Heidelberg},
 	series = {Lecture {Notes} in {Computer} {Science}},
 	title = {Type {Classes} and {Overloading} {Resolution} via {Order}-{Sorted} {Unification}},
 	volume = {523},
 	isbn = {978-3-540-47599-6},
 	booktitle = {Functional {Programming} {Languages} and {Computer} {Architecture}},
 	publisher = {Springer},
 	author = {Nipkow, Tobias and Snelting, Gregor},
 	editor = {Hughes, John},
 	year = {1991},
 	pages = {1--14},
 }
 @article{milehins_conditional_2021,
 	title = {Conditional {Transfer} {Rule}},
 	journal = {Archive of Formal Proofs},
 	author = {Milehins, Mihails},
 	year = {2021},
 }
 @article{kappelmann_speccheck_2021,
 	title = {{SpecCheck} - {Specification}-{Based} {Testing} for {Isabelle}/{ML}},
 	journal = {Archive of Formal Proofs},
 	author = {Kappelmann, Kevin and Bulwahn, Lukas and Willenbrink, Sebastian},
 	year = {2021},
 }
+@book{cain_nine_2019,
+	address = {Lisbon},
+	title = {Nine {Chapters} on the {Semigroup} {Art}},
+	author = {Cain, Alan J},
+	year = {2019},
+}
\ No newline at end of file