X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdidactic%2Finduction.ma;h=2296666c70682aa7374983c374fc5590663b7a04;hb=1ee5193677b8e2a80d4f068ee79ecac335de1196;hp=aa7b7aff6d7a742d4ac5359bb34434c890b0ba64;hpb=f0643b9fd4160f49c0d368855d0e3e638f2d58ca;p=helm.git

diff --git a/helm/software/matita/contribs/didactic/induction.ma b/helm/software/matita/contribs/didactic/induction.ma
index aa7b7aff6..2296666c7 100644
--- a/helm/software/matita/contribs/didactic/induction.ma
+++ b/helm/software/matita/contribs/didactic/induction.ma
@@ -190,7 +190,7 @@ let rec sem (v: nat → nat) (F: Formula) on F ≝
 *)
 definition if_then_else ≝ λT:Type.λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
 notation > "'if' term 19 e 'then' term 19 t 'else' term 90 f" non associative with precedence 90 for @{ 'if_then_else $e $t $f }.
-notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 90 for @{ 'if_then_else _ $e $t $f }.
+notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 90 for @{ 'if_then_else $e $t $f }.
 interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else _ e t f).
 notation < "[[ \nbsp term 19 a \nbsp ]] \nbsp \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.
 notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.