X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Flambda%2Flambda_notation.ma;fp=matita%2Fmatita%2Flib%2Flambda%2Flambda_notation.ma;h=0000000000000000000000000000000000000000;hb=46e87acb755894f9234191d675eeb5db4f5b930b;hp=e9e84c828325405940e566980f07d0a069df1839;hpb=f8bc120b39bd74ade4e11d4d3ef4355f66c42495;p=helm.git

diff --git a/matita/matita/lib/lambda/lambda_notation.ma b/matita/matita/lib/lambda/lambda_notation.ma
deleted file mode 100644
index e9e84c828..000000000
--- a/matita/matita/lib/lambda/lambda_notation.ma
+++ /dev/null
@@ -1,106 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR THE LAMBDA CALCULUS *)
-(* equivalence, invariance *)
-
-notation "hvbox(a break ≅ b)" 
-  non associative with precedence 45
-  for @{'Eq $a $b}.
-
-notation "hvbox(a break (≅ ^ term 90 c) b)"
-  non associative with precedence 45
-  for @{'Eq1 $c $a $b}.
-
-notation "hbox(! term 55 a)"
-  non associative with precedence 55
-  for @{'Invariant $a}.
-
-notation "hbox((! ^ term 90 b) term 55 a)"
-  non associative with precedence 55
-  for @{'Invariant1 $a $b}.
-
-(* lifting, substitution *)
-
-notation "hvbox(↑ [ p break , k ] break t)"
-   non associative with precedence 55
-   for @{'Lift1 $p $k $t}.
-
-notation "hvbox(M break [ / l ])"
-   non associative with precedence 90
-   for @{'Subst $M $l}.
-
-notation "hvbox(M break [ k ≝ N ])" 
-   non associative with precedence 90
-   for @{'Subst1 $M $k $N}.
-
-(* type judgements *)
-
-notation "hvbox(G break  ⊢ A break : B)"
-   non associative with precedence 45
-   for @{'TJ $G $A $B}.
-
-notation "hvbox(G break  ⊢ A break ÷ B)"
-   non associative with precedence 45
-   for @{'TJ0 $G $A $B}.
-
-(* interpretations *)
-
-notation "hvbox(║T║)"
-   non associative with precedence 55
-   for @{'IInt $T}.
-
-notation "hvbox(║T║ break _ [E])"
-   non associative with precedence 55
-   for @{'IInt1 $T $E}.
-
-notation "hvbox(║T║ break _ [E1 break , E2])"
-   non associative with precedence 55
-   for @{'IInt2 $T $E1 $E2}.
-
-notation "hvbox(║T║ * break _ [E])"
-   non associative with precedence 55
-   for @{'IIntS1 $T $E}.
-
-notation "hvbox(〚T〛)"
-   non associative with precedence 55
-   for @{'EInt $T}.
-
-notation "hvbox(〚T〛 break _ [E])"
-   non associative with precedence 55
-   for @{'EInt1 $T $E}.
-
-notation "hvbox(〚T〛 break _ [E1 break , E2])"
-   non associative with precedence 55
-   for @{'EInt2 $T $E1 $E2}.
-
-notation "hvbox(《T》)"
-   non associative with precedence 55
-   for @{'XInt $T}.
-
-notation "hvbox(《T》 break _ [E])"
-   non associative with precedence 55
-   for @{'XInt1 $T $E}.
-
-notation "hvbox(《T》 break _ [E1 break , E2])"
-   non associative with precedence 55
-   for @{'XInt2 $T $E1 $E2}.
-
-notation "hvbox(𝕂{G})"
-   non associative with precedence 55
-   for @{'IK $G}.
-
-notation "hvbox(𝕂{T} break _ [G])"
-   non associative with precedence 55
-   for @{'IK $T $G}.