| changeset 42517 | b68e1c27709a |
| parent 42510 | b9c106763325 |
| child 42665 | e4c5c7ffceea |
--- a/doc-src/IsarImplementation/Thy/ML.thy Sun May 01 17:41:49 2011 +0200 +++ b/doc-src/IsarImplementation/Thy/ML.thy Sun May 01 17:42:21 2011 +0200 @@ -699,9 +699,9 @@ \end{matharray} @{rail " - @@{ML_antiquotation let} ((term + @@{keyword \"and\"}) '=' term + @@{keyword \"and\"}) + @@{ML_antiquotation let} ((term + @'and') '=' term + @'and') ; - @@{ML_antiquotation note} (thmdef? thmrefs + @@{keyword \"and\"}) + @@{ML_antiquotation note} (thmdef? thmrefs + @'and') "} \begin{description}