Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned paper
authorChristian Urban <urbanc@in.tum.de>
Sat, 09 Apr 2011 00:29:40 +0100
changeset 2757 cdc96d79bbba
parent 2756 a6b4d9629b1c (current diff)
parent 2755 2ef9f2d61b14 (diff)
child 2758 6ba52f3a1542
tuned paper
Pearl-jv/Paper.thy file | annotate | diff | comparison | revisions 
--- a/Pearl-jv/Paper.thy	Sat Apr 09 00:28:53 2011 +0100
+++ b/Pearl-jv/Paper.thy	Sat Apr 09 00:29:40 2011 +0100
@@ -68,7 +68,7 @@
   Pitts at al \cite{GabbayPitts02,Pitts03}, whose most basic notion is
   a sort-respecting permutation operation defined over a countably
   infinite collection of sorted atoms. The aim of this paper is to
-  describe how to adapt this work so that it can be implemented in a
+  describe how we adapted this work so that it can be implemented in a
   theorem prover based on Higher-Order Logic (HOL). For this we
   present the definition we made in the implementation and also review
   many proofs. There are a two main design choices to be made. One is
nominal2