RELATIONAL: new undecomposable definition of NLE

[helm.git] / helm / software / matita / help / C / sec_tactics.xml

diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index cad04a53c400a3ab17ba867ca49fe9429aedc5b0..193a0e3310f489c1c587955cc1a3210deed2f4a3 100644 (file)
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -522,7 +522,7 @@
             For each each premise <command>H</command> 
             of type <command>T</command> in the current context
             where <command>T</command> is a non-recursive inductive type
-            withour right parameters, the tactic runs
+            of sort Prop without right parameters, the tactic runs
             <command> 
              elim H as H<subscript>1</subscript> ... H<subscript>m</subscript>
             </command>, clears <command>H</command>  and runs itself