refactoring ...

[helm.git] / matita / matita / contribs / lambda / terms / parallel_computation.ma

diff --git a/matita/matita/contribs/lambda/terms/parallel_computation.ma b/matita/matita/contribs/lambda/terms/parallel_computation.ma
index 4f93f90a7b19032cca45648dae8e954789fb59f7..3b048d1336cb83a24c4fff0a24e5dd1cf1cfed10 100644 (file)
--- a/matita/matita/contribs/lambda/terms/parallel_computation.ma
+++ b/matita/matita/contribs/lambda/terms/parallel_computation.ma
@@ -21,10 +21,6 @@ definition preds: relation term ≝ star … pred.
 interpretation "parallel computation"
    'ParRedStar M N = (preds M N).
 
-notation "hvbox( M ⤇* break term 46 N )"
-   non associative with precedence 45
-   for @{ 'ParRedStar $M $N }.
-
 lemma preds_refl: reflexive … preds.
 //
 qed.