Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
doc-src/Codegen/Thy/Foundations.thy
changeset 46521 addcdf0dd283
parent 45211 3dd426ae6bea 
--- a/doc-src/Codegen/Thy/Foundations.thy	Sat Feb 18 20:12:16 2012 +0100
+++ b/doc-src/Codegen/Thy/Foundations.thy	Sat Feb 18 20:12:30 2012 +0100
@@ -117,7 +117,7 @@
   interface, transforming a list of function theorems to another list
   of function theorems, provided that neither the heading constant nor
   its type change.  The @{term "0\<Colon>nat"} / @{const Suc} pattern
-  elimination implemented in theory @{theory Efficient_Nat} (see
+  elimination implemented in theory @{text Efficient_Nat} (see
   \secref{eff_nat}) uses this interface.
 
   \noindent The current setup of the preprocessor may be inspected
isabelle