
@book{urban_isabelle_2019,
	title = {The {Isabelle} {Cookbook}: {A} {Gentle} {Tutorial} for {Programming} {Isabelle}/{ML}},
	urldate = {2018-09-13},
	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},
	file = {progtutorial (7).pdf:/Users/mihailsmilehins/Library/Mobile Documents/com~apple~CloudDocs/zotero-data/storage/M7CPVV49/progtutorial (7).pdf:application/pdf},
}

@unpublished{wenzel_isabelle/isar_2019,
	title = {The {Isabelle}/{Isar} {Implementation}},
	language = {en},
	author = {Wenzel, Makarius},
	collaborator = {Berghofer, Stefan and Haftmann, Florian and Paulson, Larry},
	year = {2019},
	file = {Wenzel - The IsabelleIsar Implementation.pdf:/Users/mihailsmilehins/Library/Mobile Documents/com~apple~CloudDocs/zotero-data/storage/8QXHPVK6/Wenzel - The IsabelleIsar Implementation.pdf:application/pdf},
}

@unpublished{wenzel_isabelle/isar_2019-1,
	title = {The {Isabelle}/{Isar} {Reference} {Manual}},
	language = {en},
	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},
	file = {Wenzel - The IsabelleIsar Reference Manual.pdf:/Users/mihailsmilehins/Library/Mobile Documents/com~apple~CloudDocs/zotero-data/storage/9CPYJCHX/Wenzel - The IsabelleIsar Reference Manual.pdf:application/pdf},
}

@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},
}

@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},
	file = {ScienceDirect Snapshot:/Users/mihailsmilehins/Library/Mobile Documents/com~apple~CloudDocs/zotero-data/storage/PF5HRFMM/0743106686900154.html:text/html;Submitted Version:/Users/mihailsmilehins/Library/Mobile Documents/com~apple~CloudDocs/zotero-data/storage/FMC65UNW/Paulson - 1986 - Natural deduction as higher-order resolution.pdf:application/pdf},
}

@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},
	file = {Kun{\v c}ar and Popescu - 2017 - Comprehending IsabelleHOL{\textquoteright}s Consistency.pdf:/Users/mihailsmilehins/Library/Mobile Documents/com~apple~CloudDocs/zotero-data/storage/DMJLJVSL/Kun{\v c}ar and Popescu - 2017 - Comprehending IsabelleHOL{\textquoteright}s Consistency.pdf:application/pdf},
}

@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},
	file = {Wenzel - 1999 - Isar {\textemdash} A Generic Interpretative Approach to Readab.pdf:/Users/mihailsmilehins/Library/Mobile Documents/com~apple~CloudDocs/zotero-data/storage/BBQ426IY/Wenzel - 1999 - Isar {\textemdash} A Generic Interpretative Approach to Readab.pdf:application/pdf},
}

@article{wenzel_isabelleisar_2007,
	title = {Isabelle/{Isar} {\textemdash} a {Generic} {Framework} for {Human}-{Readable} {Proof} {Documents}},
	volume = {10},
	language = {en},
	number = {23},
	journal = {Studies in Logic, Grammar and Rhetoric},
	author = {Wenzel, Makarius},
	year = {2007},
	pages = {277--297},
	file = {Wenzel - IsabelleIsar {\textemdash} a Generic Framework for Human-Read.pdf:/Users/mihailsmilehins/Library/Mobile Documents/com~apple~CloudDocs/zotero-data/storage/AQIX26VS/Wenzel - IsabelleIsar {\textemdash} a Generic Framework for Human-Read.pdf:application/pdf},
}

@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)},
	file = {Milner - 1997 - The definition of standard ML revised.pdf:/Users/mihailsmilehins/Library/Mobile Documents/com~apple~CloudDocs/zotero-data/storage/9Q2BB5XT/Milner - 1997 - The definition of standard ML revised.pdf:application/pdf},
}
