# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1356879528 0
# Node ID f7896d90aa19af1cf725b11cc465c6af88c54cf8
# Parent  50880fcda34da4bbb07972e3c42c534dce15b9a6
more

diff -r 50880fcda34d -r f7896d90aa19 Paper.thy
--- 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 {*
diff -r 50880fcda34d -r f7896d90aa19 document/root.bib
--- /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}
+}
diff -r 50880fcda34d -r f7896d90aa19 document/root.tex
--- 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}
 
diff -r 50880fcda34d -r f7896d90aa19 paper.pdf
Binary file paper.pdf has changed