| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Doc/Sugar/document/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 898 B |
|
Quelle root.tex Sprache: Latech |
|||||||||
|
\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym} \usepackage{amssymb} \usepackage{mathpartir} % this should be the last package used \usepackage{pdfsetup} % urls in roman style, theory text in math-similar italics \urlstyle{rm} \isabellestyle{it} \newcommand{\showout}{\mbox{}\hspace{-2em}$\leadsto$\quad} \hyphenation{Isa-belle} \begin{document} \title{\LaTeX\ Sugar for Isabelle Documents} \author{Florian Haftmann, Gerwin Klein, Tobias Nipkow, Norbert Schirmer} \maketitle \begin{abstract} This document shows how to typset mathematics in Isabelle-based documents in a style close to that in ordinary computer science papers. \end{abstract} %\tableofcontents % generated text of all theories \input{Sugar.tex} % optional bibliography \bibliographystyle{abbrv} \bibliography{root} \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28