Most of the time, URIs can now be replaced with identifiers in "interpretation".

[helm.git] / helm / software / matita / contribs / dama / dama / cprop_connectives.ma

diff --git a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
index a53961733a72d11f0870538a3f87858555b89772..91a2335c7998f44e40589b0cbd7751c64db3d680 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
+++ b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
@@ -18,25 +18,21 @@ inductive Or (A,B:CProp) : CProp ≝
    Left : A → Or A B
  | Right : B → Or A B.
 
-interpretation "constructive or" 'or x y =
-  (cic:/matita/dama/cprop_connectives/Or.ind#xpointer(1/1) x y).
+interpretation "constructive or" 'or x y = (Or x y).
 
 inductive And (A,B:CProp) : CProp ≝
  | Conj : A → B → And A B.
  
-interpretation "constructive and" 'and x y =
-  (cic:/matita/dama/cprop_connectives/And.ind#xpointer(1/1) x y).
+interpretation "constructive and" 'and x y = (And x y).
 
 inductive exT (A:Type) (P:A→CProp) : CProp ≝
   ex_introT: ∀w:A. P w → exT A P.
 
-interpretation "CProp exists" 'exists \eta.x =
-  (cic:/matita/dama/cprop_connectives/exT.ind#xpointer(1/1) _ x).
+interpretation "CProp exists" 'exists \eta.x = (exT _ x).
 
 definition Not : CProp → Prop ≝ λx:CProp.x → False.
 
-interpretation "constructive not" 'not x = 
-  (cic:/matita/dama/cprop_connectives/Not.con x).
+interpretation "constructive not" 'not x = (Not x).
   
 definition cotransitive ≝
  λC:Type.λlt:C→C→CProp.∀x,y,z:C. lt x y → lt x z ∨ lt z y.