- tps_tpr closed! (substitution is a reduction)

[helm.git] / matita / matita / lib / lambda-delta / xoa_notation.ma

diff --git a/matita/matita/lib/lambda-delta/xoa_notation.ma b/matita/matita/lib/lambda-delta/xoa_notation.ma
index ce9460eb6f7c3deb2cd602146efe0e64c95bc4ec..b8270b6602e48a10c5801be709b2f0c54390fa43 100644 (file)
--- a/matita/matita/lib/lambda-delta/xoa_notation.ma
+++ b/matita/matita/lib/lambda-delta/xoa_notation.ma
@@ -136,9 +136,3 @@ notation "hvbox(∨∨ term 29 P0 break | term 29 P1 break | term 29 P2 break |
  non associative with precedence 30
  for @{ 'Or $P0 $P1 $P2 $P3 }.
 
-(* multiple conjunction connective (3) *)
-
-notation "hvbox(∧∧ term 34 P0 break & term 34 P1 break & term 34 P2)"
- non associative with precedence 35
- for @{ 'And $P0 $P1 $P2 }.
-