# HG changeset patch # User kleing # Date 1194003327 -3600 # Node ID d0928156e326c457822e58c3a39c7cf5223c8f91 # Parent 3dc292be0b5476c182891593b714d8d5e0976121 Added reference to Jeremy Dawson's paper on the word library. Added header to remaining word/*.thy files so they show up in toc. diff -r 3dc292be0b54 -r d0928156e326 src/HOL/Word/Examples/WordExamples.thy --- a/src/HOL/Word/Examples/WordExamples.thy Fri Nov 02 08:59:15 2007 +0100 +++ b/src/HOL/Word/Examples/WordExamples.thy Fri Nov 02 12:35:27 2007 +0100 @@ -5,6 +5,8 @@ Examples demonstrating and testing various word operations. *) +header "Examples of word operations" + theory WordExamples imports WordMain begin diff -r 3dc292be0b54 -r d0928156e326 src/HOL/Word/Size.thy --- a/src/HOL/Word/Size.thy Fri Nov 02 08:59:15 2007 +0100 +++ b/src/HOL/Word/Size.thy Fri Nov 02 12:35:27 2007 +0100 @@ -5,6 +5,9 @@ A typeclass for parameterizing types by size. Used primarily to parameterize machine word sizes. *) + +header "The size class" + theory Size imports Numeral_Type begin diff -r 3dc292be0b54 -r d0928156e326 src/HOL/Word/TdThs.thy --- a/src/HOL/Word/TdThs.thy Fri Nov 02 08:59:15 2007 +0100 +++ b/src/HOL/Word/TdThs.thy Fri Nov 02 12:35:27 2007 +0100 @@ -10,6 +10,8 @@ theory TdThs imports Main begin +section "More lemmas about normal type definitions" + lemma tdD1: "type_definition Rep Abs A \ \x. Rep x \ A" and tdD2: "type_definition Rep Abs A \ \x. Abs (Rep x) = x" and diff -r 3dc292be0b54 -r d0928156e326 src/HOL/Word/document/root.tex --- a/src/HOL/Word/document/root.tex Fri Nov 02 08:59:15 2007 +0100 +++ b/src/HOL/Word/document/root.tex Fri Nov 02 12:35:27 2007 +0100 @@ -14,6 +14,11 @@ \maketitle +\begin{abstract} +A formalisation of generic, fixed size machine words in Isabelle/HOL. An earlier version of this +formalisation is described in \cite{dawson-avocs07}. +\end{abstract} + \tableofcontents \begin{center} @@ -28,4 +33,7 @@ \parindent 0pt\parskip 0.5ex \input{session} +\bibliographystyle{plain} +\bibliography{root} + \end{document}