dependences update

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Legacy-2 / preamble.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma
index a2c8a84ed1358d82d02d60b2a1c5694c54af07d1..00c38151d1826bb28550294d28b98cf11ca1c0b9 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Legacy-1/definitions.ma".
+include "Legacy-1/theory.ma".
 
 default "equality"
  cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq.ind
@@ -34,15 +34,25 @@ default "false"
 default "absurd"
  cic:/matita/LAMBDA-TYPES/Legacy-1/coq/props/absurd.con. 
 
-interpretation "Coq's natural plus" 'plus x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/plus.con x y).
-interpretation "Coq's natural minus" 'minus x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/minus.con x y).
-interpretation "Coq's logical and" 'and x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/land.ind#xpointer(1/1) x y).
-interpretation "Coq's logical or" 'or x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/or.ind#xpointer(1/1) x y).
-interpretation "Coq's logical not" 'not x = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/not.con x).
-interpretation "Coq's exists" 'exists \eta.x = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/ex.ind#xpointer(1/1) _ x).
-interpretation "Coq's natural 'less or equal to'" 'leq x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/le.ind#xpointer(1/1) x y).
-interpretation "Coq's natural 'less than'" 'lt x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/lt.con x y).
-interpretation "Coq's leibnitz's equality" 'eq x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq.ind#xpointer(1/1) _ x y).
+interpretation "Coq 7.3.1 natural plus" 'plus x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/plus.con x y).
+interpretation "Coq 7.3.1 natural minus" 'minus x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/minus.con x y).
+interpretation "Coq 7.3.1 logical and" 'and x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/land.ind#xpointer(1/1) x y).
+interpretation "Coq 7.3.1 logical or" 'or x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/or.ind#xpointer(1/1) x y).
+interpretation "Coq 7.3.1 logical not" 'not x = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/not.con x).
+interpretation "Coq 7.3.1 exists" 'exists \eta.x = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/ex.ind#xpointer(1/1) ? x).
+interpretation "Coq 7.3.1 natural 'less or equal to'" 'leq x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/le.ind#xpointer(1/1) x y).
+interpretation "Coq 7.3.1 natural 'less than'" 'lt x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/lt.con x y).
+interpretation "Coq 7.3.1 leibnitz's equality" 'eq t x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq.ind#xpointer(1/1) t x y).
+
+alias symbol "plus" = "Coq 7.3.1 natural plus".
+alias symbol "minus" = "Coq 7.3.1 natural minus".
+alias symbol "and" = "Coq 7.3.1 logical and".
+alias symbol "or" = "Coq 7.3.1 logical or".
+alias symbol "not" = "Coq 7.3.1 logical not".
+alias symbol "exists" = "Coq 7.3.1 exists".
+alias symbol "leq" = "Coq 7.3.1 natural 'less or equal to'".
+alias symbol "lt" = "Coq 7.3.1 natural 'less than'".
+alias symbol "eq" = "Coq 7.3.1 leibnitz's equality".
 
 theorem f_equal_sym: \forall A,B:Set.\forall f:A\to B.\forall x,y.
                      x = y \to (f y) = (f x).