Mercurial Mercurial > hg > tm / 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.
fixed compilation of paper and typo
authorChristian Urban <christian dot urban at kcl dot ac dot uk>
Sun, 10 Feb 2013 20:56:08 +0000
changeset 164 8a3e63163910
parent 163 67063c5365e1
child 165 582916f289ea
fixed compilation of paper and typo
Paper/Paper.thy file | annotate | diff | comparison | revisions
Paper/ROOT.ML file | annotate | diff | comparison | revisions
paper.pdf file | annotate | diff | comparison | revisions 
--- a/Paper/Paper.thy	Sun Feb 10 19:49:07 2013 +0000
+++ b/Paper/Paper.thy	Sun Feb 10 20:56:08 2013 +0000
@@ -1296,7 +1296,7 @@
   \begin{center}
   \begin{tabular}{c@ {\hspace{4mm}}c}
   \begin{tabular}{rcl@ {\hspace{4mm}}l}
-  @{term r} & @{text "::="} & @{term z} & (zero-functions)\\
+  @{term r} & @{text "::="} & @{term z} & (zero-function)\\
             & @{text "|"}   & @{term s} & (successor-function)\\
             & @{text "|"}   & @{term "id n m"} & (projection)\\
   \end{tabular} &
--- a/Paper/ROOT.ML	Sun Feb 10 19:49:07 2013 +0000
+++ b/Paper/ROOT.ML	Sun Feb 10 20:56:08 2013 +0000
@@ -1,9 +1,9 @@
 no_document 
-use_thys ["../thys/turing_basic", 
-          "../thys/turing_hoare",
-          "../thys/uncomputable", 
-          "../thys/abacus"(*,
-          "../thys/rec_def",
-          "../thys/recursive"*)];
+use_thys ["../thys/Turing", 
+          "../thys/Turing_Hoare",
+          "../thys/Uncomputable", 
+          "../thys/Abacus",
+          "../thys/Rec_Def",
+          "../thys/Recursive"];
 
 use_thys ["Paper"]
Binary file paper.pdf has changed
tm