X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_terms.xml;h=d521ac87060a6a2e0a462fd8ae079e2235184696;hb=48aa99d1d9659e55d68ab3ef50b10bc6165eee03;hp=30692211e93b52de3dc55fa181dd3532fedc581e;hpb=14eaf9296ca8a24b715261a98898fab3104554f0;p=helm.git diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml index 30692211e..d521ac870 100644 --- a/helm/software/matita/help/C/sec_terms.xml +++ b/helm/software/matita/help/C/sec_terms.xml @@ -479,7 +479,7 @@ Notice that the command is equivalent to definition f: T ≝ t. - <emphasis role="bold">variant</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;] + <emphasis role="bold">variant</emphasis> &id;<emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> &term; variant variant f: T ≝ t Same as theorem f: T ≝ t, but it does not