Quelle root.tex Sprache: Latech

\documentclass[a4paper,fleqn]{article}
\usepackage[T1]{fontenc}
\usepackage{graphicx}
\usepackage[refpage]{nomencl}
\usepackage{iman,extra,isar}
\usepackage{isabelle,isabellesym}
\usepackage{style}
\usepackage{mathpartir}
\usepackage{amsthm}
\usepackage{pdfsetup}

\newcommand{\cmd}[1]{\isacommand{#1}}

\newcommand{\isasymINFIX}{\cmd{infix}}
\newcommand{\isasymLOCALE}{\cmd{locale}}
\newcommand{\isasymINCLUDES}{\cmd{includes}}
\newcommand{\isasymDATATYPE}{\cmd{datatype}}
\newcommand{\isasymDEFINES}{\cmd{defines}}
\newcommand{\isasymNOTES}{\cmd{notes}}
\newcommand{\isasymCLASS}{\cmd{class}}
\newcommand{\isasymINSTANCE}{\cmd{instance}}
\newcommand{\isasymLEMMA}{\cmd{lemma}}
\newcommand{\isasymPROOF}{\cmd{proof}}
\newcommand{\isasymQED}{\cmd{qed}}
\newcommand{\isasymFIX}{\cmd{fix}}
\newcommand{\isasymASSUME}{\cmd{assume}}
\newcommand{\isasymSHOW}{\cmd{show}}
\newcommand{\isasymNOTE}{\cmd{note}}
\newcommand{\isasymCODEGEN}{\cmd{code\_gen}}
\newcommand{\isasymPRINTCODETHMS}{\cmd{print\_codethms}}
\newcommand{\isasymFUN}{\cmd{fun}}
\newcommand{\isasymFUNCTION}{\cmd{function}}
\newcommand{\isasymPRIMREC}{\cmd{primrec}}
\newcommand{\isasymRECDEF}{\cmd{recdef}}

\newcommand{\qt}[1]{``#1''}
\newcommand{\qtt}[1]{"{}{#1}"{}}
\newcommand{\qn}[1]{\emph{#1}}
\newcommand{\strong}[1]{{\bfseries #1}}
\newcommand{\fixme}[1][!]{\strong{FIXME: #1}}

\newtheorem{exercise}{Exercise}{\bf}{\itshape}
%\newtheorem*{thmstar}{Theorem}{\bf}{\itshape}

\hyphenation{Isabelle}
\hyphenation{Isar}

\isadroptag{theory}
\title{Defining Recursive Functions in Isabelle/HOL}
\author{Alexander Krauss}

\isabellestyle{tt}

\begin{document}

\date{\ \\}
\maketitle

\begin{abstract}
This tutorial describes the use of the \emph{function} package,
which provides general recursive function definitions for Isabelle/HOL.
We start with very simple examples and then gradually move on to more
advanced topics such as manual termination proofs, nested recursion,
partiality, tail recursion and congruence rules.
\end{abstract}

%\thispagestyle{empty}\clearpage

%\pagenumbering{roman}
%\clearfirst

\input{intro.tex}
\input{Functions.tex}
%\input{conclusion.tex}

\begingroup
%\tocentry{\bibname}
\bibliographystyle{plain} \small\raggedright\frenchspacing
\bibliography{manual}
\endgroup

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:

quality100%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.