Fix the build of simple wallet document

.gitignore

@@ -46,6 +46,7 @@ lem/.hollogs
 tester/*.native
 tester/_build
 output/
+simplewallet/
 tester/coverage/
 tester/bisect*.out
 *.marks

Makefile

@@ -29,7 +29,7 @@ document/output.pdf: ContractSem.thy RelationalSem.thy example/Deed.thy document
 	sh document_generation.sh
 
 simplewallet: document/simplewallet.pdf
-document/simplewallet.pdf: ContractSem.thy RelationalSem.thy example/Deed.thy document/root.tex lem/Evm.thy lem/Word256.thy lem/Word160.thy lem/Word8.thy lem/Keccak.thy
+document/simplewallet.pdf: ContractSem.thy RelationalSem.thy example/Deed.thy simple_wallet_document/root.tex lem/Evm.thy lem/Word256.thy lem/Word160.thy lem/Word8.thy lem/Keccak.thy
 	sh wallet_generation.sh
 
 lem-thy: lem/Block.thy lem/Evm.thy lem/Keccak.thy lem/Rlp.thy lem/Word160.thy lem/Word256.thy lem/Word8.thy lem/Keccak.thy lem/Word4.thy

ROOT

@@ -55,9 +55,12 @@ session "simplewallet" = "HOL" +
     "lem/Word8"
     "lem/Keccak"
     "lem/Evm"
+	"Hoare"
+	"HoareTripleForInstructions"
+	"HoareTripleForInstructions2"
   theories
     "example/SimpleWallet"
-  document_files
+  document_files (in simple_wallet_document)
     "root.tex"
 
 

simple_wallet_document/root.tex

@@ -0,0 +1,67 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage{isabelle,isabellesym}
+
+% further packages required for unusual symbols (see also
+% isabellesym.sty), use only when needed
+
+%\usepackage{amssymb}
+  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
+  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
+  %\<triangleq>, \<yen>, \<lozenge>
+
+%\usepackage{eurosym}
+  %for \<euro>
+
+%\usepackage[only,bigsqcap]{stmaryrd}
+  %for \<Sqinter>
+
+%\usepackage{eufrak}
+  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
+
+%\usepackage{textcomp}
+  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
+  %\<currency>
+
+% 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{A simple wallet}
+\author{Yoichi Hirai\footnote{\texttt{i@yoichihirai.com}}}
+\maketitle
+
+\tableofcontents
+
+% sane default for proof documents
+\parindent 0pt\parskip 0.5ex
+
+\newpage
+
+\begin{itemize}
+\item This document is produced from the code available at
+\url{https://github.com/pirapira/eth-isabelle}.
+\item To get updates on this project and similar ones, follow \url{http://gitter.im/ethereum/formal-methods}.
+\end{itemize}
+
+% generated text of all theories
+\input{session}
+
+% optional bibliography
+%\bibliographystyle{abbrv}
+%\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End: