Cite Isar Ref

Author: jacobmischka

src/proof-assistants.bib

@@ -67,3 +67,16 @@ @article{Alloy
 	keywords = {first-order logic, Object models, Z specification language}
 }
 
+@manual{ProgProve,
+	author = {Nipkow, Tobias},
+	title = {Programming and Proving in Isabelle/HOL},
+	year = {2020},
+	date = {2020-04-15}
+}
+
+@manual{IsarRef,
+	title = {The Isabelle/Isar Reference Manual},
+	author = {Wenzel, Makarius},
+	year = {2020},
+	date = {2020-04-15}
+}

src/thesis.tex

@@ -589,17 +589,18 @@ \chapter{Incremental Soundness}
 many advanced features and slightly nuanced ways to perform similar tasks.
 
 An Isabelle proof can consist of several distinct but related types of syntax.
-The most common and \textit{de facto} framework used in modern Isabelle proofs
-is Isabelle/Isar, which is modeled after human-readable logical proofs.
+The most common and recommended framework used in modern Isabelle proofs is
+Isabelle/Isar, which is modeled after human-readable logical
+proofs\cite{IsarRef}.
 In addition to the structured Isar syntax, logical steps also can be applied
 individually using the older \textit{apply script} syntax.
 The Isar and apply script syntaxes can be interwoven, resulting in a
 jarring shift when encountered by a less expert user.
 In addition to the two primary \textit{inner} proof syntaxes which perform the
 specifications and proofs, Isabelle proofs must make use of another layer of
 \textit{outer} syntax of Isabelle types and logical terms, an object-logic,
-which is most commonly Isabelle/HOL (higher-order logic). Additionally, logical
-rules can be defined using the Isabelle/Pure syntax.
+which is most commonly Isabelle/HOL (higher-order logic).
+Additionally, logical rules can be defined using the Isabelle/Pure syntax.
 As a result, in order to become productive with Isabelle one must
 learn many different sublanguages; particularly so when diving into
 a large proof that makes extensive use of more advanced features of each.
@@ -633,7 +634,6 @@ \chapter{Incremental Soundness}
 Tail call remains a phase 3 proposal currently in the implementation
 phase\cite{WasmProposals}.
 
-
 \section{Non-trapping Float-to-Int Conversions}
 
 The first of the three mechanized, this proposal introduces 8 new floating