equal
deleted
inserted
replaced
10 \usepackage{multicol} |
10 \usepackage{multicol} |
11 \usepackage{stmaryrd} |
11 \usepackage{stmaryrd} |
12 %\usepackage[scaled=.85]{beramono} |
12 %\usepackage[scaled=.85]{beramono} |
13 \usepackage{isabelle,iman,pdfsetup} |
13 \usepackage{isabelle,iman,pdfsetup} |
14 |
14 |
15 \newcommand\download{\url{http://www21.in.tum.de/~blanchet/\#software}} |
15 \newcommand\download{\url{http://isabelle.in.tum.de/components/}} |
16 |
16 |
17 \def\qty#1{\ensuremath{\left<\mathit{#1\/}\right>}} |
17 \def\qty#1{\ensuremath{\left<\mathit{#1\/}\right>}} |
18 \def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1\/}}\right>}$} |
18 \def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1\/}}\right>}$} |
19 |
19 |
20 \newcommand\const[1]{\textsf{#1}} |
20 \newcommand\const[1]{\textsf{#1}} |
863 by Daniel K\"uhlwein that implements strategy scheduling on top of E. To use |
863 by Daniel K\"uhlwein that implements strategy scheduling on top of E. To use |
864 E-MaLeS, set the environment variable \texttt{E\_MALES\_HOME} to the directory |
864 E-MaLeS, set the environment variable \texttt{E\_MALES\_HOME} to the directory |
865 that contains the \texttt{emales.py} script. Sledgehammer has been tested with |
865 that contains the \texttt{emales.py} script. Sledgehammer has been tested with |
866 version 1.1. |
866 version 1.1. |
867 |
867 |
|
868 \item[\labelitemi] \textbf{\textit{e\_par}:} E-Par is a metaprover developed |
|
869 by Josef Urban that implements strategy scheduling on top of E. To use |
|
870 E-Par, set the environment variable \texttt{E\_HOME} to the directory |
|
871 that contains the \texttt{runepar.pl} script and the \texttt{eprover} and |
|
872 \texttt{epclextract} executables, or use the prebuilt E package from \download. |
|
873 |
868 \item[\labelitemi] \textbf{\textit{iprover}:} iProver is a pure |
874 \item[\labelitemi] \textbf{\textit{iprover}:} iProver is a pure |
869 instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}. |
875 instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}. |
870 To use iProver, set the environment variable \texttt{IPROVER\_HOME} to the |
876 To use iProver, set the environment variable \texttt{IPROVER\_HOME} to the |
871 directory that contains the \texttt{iprover} and \texttt{vclausify\_rel} |
877 directory that contains the \texttt{iprover} and \texttt{vclausify\_rel} |
872 executables. Sledgehammer has been tested with version 0.99. |
878 executables. Sledgehammer has been tested with version 0.99. |