Mercurial Mercurial > repos > isabelle / 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;
authorwenzelm
Sat, 27 Jul 2013 16:44:40 +0200
changeset 52733 98f94010d78d
parent 52732 b4da1f2ec73f
child 52734 077149654ab4
tuned;
src/Doc/IsarImplementation/ML.thy file | annotate | diff | comparison | revisions 
--- a/src/Doc/IsarImplementation/ML.thy	Sat Jul 27 16:35:51 2013 +0200
+++ b/src/Doc/IsarImplementation/ML.thy	Sat Jul 27 16:44:40 2013 +0200
@@ -251,7 +251,7 @@
   T}, with variants as for types
 
   \item certified terms are called @{ML_text ct}, rarely @{ML_text
-  t}, with variants as for terms
+  t}, with variants as for terms (never @{ML_text ctrm})
 
   \item theorems are called @{ML_text th}, or @{ML_text thm}
isabelle