From 59214186b817329342d9d72e23adf12f7a3b1348 Mon Sep 17 00:00:00 2001 From: stuebinm Date: Sat, 29 Jun 2024 21:31:22 +0200 Subject: had some fun writing an IsabelleHOL backend (do not actually use this, most things are broken, and the primitives lib barely exists and is simply incorrect. But it is enough to create syntax-correct Isabelle code for relatively simply rust code, as long as it does not contain any uses of traits) --- backends/IsabelleHOL/document/root.tex | 60 ++++++++++++++++++++++++++++++++++ 1 file changed, 60 insertions(+) create mode 100644 backends/IsabelleHOL/document/root.tex (limited to 'backends/IsabelleHOL/document') diff --git a/backends/IsabelleHOL/document/root.tex b/backends/IsabelleHOL/document/root.tex new file mode 100644 index 00000000..63ac8e42 --- /dev/null +++ b/backends/IsabelleHOL/document/root.tex @@ -0,0 +1,60 @@ +\documentclass[11pt,a4paper]{article} +\usepackage[T1]{fontenc} +\usepackage{isabelle,isabellesym} + +% further packages required for unusual symbols (see also +% isabellesym.sty), use only when needed + +%\usepackage{amssymb} + %for \, \, \, \, \, \, + %\, \, \, \, \, + %\, \, \ + +%\usepackage{eurosym} + %for \ + +%\usepackage[only,bigsqcap,bigparallel,fatsemi,interleave,sslash]{stmaryrd} + %for \, \, \, \, \ + +%\usepackage{eufrak} + %for \ ... \, \ ... \ (also included in amssymb) + +%\usepackage{textcomp} + %for \, \, \, \, \, + %\ + +% 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} + + +\begin{document} + +\title{IsabelleHOL} +\author{stuebinm} +\maketitle + +\tableofcontents + +% sane default for proof documents +\parindent 0pt\parskip 0.5ex + +% generated text of all theories +\input{session} + +% optional bibliography +%\bibliographystyle{abbrv} +%\bibliography{root} + +\end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: -- cgit v1.2.3