--- a/Paper.thy	Sat Dec 29 20:17:57 2012 +0000
+++ b/Paper.thy	Sun Dec 30 14:58:48 2012 +0000
@@ -10,15 +10,16 @@
 
 text {*
 
-In earlier work, we formalised in Isabelle/HOL the correctness 
-proofs for two algorithms, one about type-checking in LF and 
-another about deciding requests in access control [???]. These 
-formalisation efforts uncovered a gap in the informal correctness 
+We formalised in earlier work the correctness 
+proofs for two algorithms in Isabelle/HOL, one about type-checking in LF and 
+another about deciding requests in access control \cite{UrbanCheneyBerghofer11} [???]: 
+these 
+formalisations uncovered a gap in the informal correctness 
 proof of the former and made us realise that important details 
 were left out in the informal model for the latter. However, 
 in both cases we were unable to formalise computablility 
-arguments. The reason is that both algorithms are formulated
-as inductive predicates. Say @{text "P"} is one such predicate.
+arguments for the algorithms. The reason is that both algorithms are formulated
+in terms of inductive predicates. Suppose @{text "P"} stands for one such predicate.
 Decidability of @{text P} usually amounts to showing whether 
 @{term "P \<or> \<not>P"} holds. But this does not work in Isabelle/HOL,
 since it is a theorem prover based on classical logic where
@@ -46,6 +47,14 @@
 
 *}
 
+
+section {* Wang Tiles *}
+
+text {*
+  Used in texture mapings - graphics
+*}
+
+
 section {* Related Work *}
 
 text {*

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/document/root.bib	Sun Dec 30 14:58:48 2012 +0000
@@ -0,0 +1,9 @@
+@article{UrbanCheneyBerghofer11,
+  author = {C.~Urban and J.~Cheney and S.~Berghofer},
+  title = {{M}echanizing the {M}etatheory of {LF}},
+  journal = {ACM Transactions on Computational Logic},
+  volume = {12},
+  issue = {2},
+  year = {2011},
+  pages = {15:1--15:42}
+}

--- a/document/root.tex	Sat Dec 29 20:17:57 2012 +0000
+++ b/document/root.tex	Sun Dec 30 14:58:48 2012 +0000
@@ -80,8 +80,8 @@
 \input{session}
 
 % optional bibliography
-%\bibliographystyle{abbrv}
-%\bibliography{root}
+\bibliographystyle{abbrv}
+\bibliography{root}
 
 \end{document}
 

Binary file paper.pdf has changed