Sort search results in order of relevance, where relevance =
a) better if 0 premises for intro or 1 premise for elim/dest rules
b) better if substitution size wrt to current goal is smaller
Only applies to intro, dest, elim, and simp
(contributed by Rafal Kolanski, NICTA)
\documentclass[envcountsame]{llncs}
%\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym,pdfsetup}
%for best-style documents ...
\urlstyle{rm}
%\isabellestyle{it}
\newcommand{\tweakskip}{\vspace{-\medskipamount}}
\pagestyle{plain}
\begin{document}
\title{%A Compact Introduction to
Structured Proofs in Isar/HOL\thanks{Published in TYPES 2002, LNCS 2646.}}
\author{Tobias Nipkow}
\institute{Institut f{\"u}r Informatik, TU M{\"u}nchen\\
{\small\url{http://www.in.tum.de/~nipkow/}}}
\date{}
\maketitle
\begin{abstract}
Isar is an extension of the theorem prover Isabelle with a language
for writing human-readable structured proofs. This paper is an
introduction to the basic constructs of this language.
% It is aimed at potential users of Isar
% but also discusses the design rationals
% behind the language and its constructs.
\end{abstract}
\input{intro.tex}
\input{Logic.tex}
\input{Induction.tex}
\small
\paragraph{Acknowledgement}
I am deeply indebted to Markus Wenzel for conceiving Isar. Clemens Ballarin,
Gertrud Bauer, Stefan Berghofer, Gerwin Klein, Norbert Schirmer,
Markus Wenzel and Freek Wiedijk commented on and improved this paper.
\begingroup
\bibliographystyle{plain} \small\raggedright\frenchspacing
\bibliography{root}
\endgroup
\end{document}