X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama_didactic%2Fbottom.ma;h=161063b426341ca18c2c8d6b6723287f35749d1f;hb=3deaedbac3407f8b4602b885a6405d4e0cc3e955;hp=bed8ec6b1a0b1f21d3e790cf3281d4212f20a090;hpb=fd4d7813792de2cd5999d444c14f7cd72e2f3ce9;p=helm.git

diff --git a/helm/software/matita/dama_didactic/bottom.ma b/helm/software/matita/dama_didactic/bottom.ma
index bed8ec6b1..161063b42 100644
--- a/helm/software/matita/dama_didactic/bottom.ma
+++ b/helm/software/matita/dama_didactic/bottom.ma
@@ -12,11 +12,13 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/test/decl".
+
 
 include "nat/times.ma".
 include "nat/orders.ma".
 
+include "decl.ma".
+
 inductive L (T:Type):Type:=
   bottom: L T
  |j: T → L T.
@@ -29,9 +31,9 @@ notation "hvbox(a break ≡ b)"
 for @{ 'equiv $a $b }.
 
 interpretation "uguaglianza parziale" 'equiv x y =
- (cic:/matita/test/decl/eq.ind#xpointer(1/1) _ x y).
+ (cic:/matita/tests/decl/eq.ind#xpointer(1/1) _ x y).
 
-coercion cic:/matita/test/decl/L.ind#xpointer(1/1/2).
+coercion cic:/matita/tests/decl/L.ind#xpointer(1/1/2).
  
 lemma sim: ∀T:Type. ∀x,y:T. (j ? x) ≡ (j ? y) → (j ? y) ≡ (j ? x).
  intros.
@@ -61,13 +63,13 @@ axiom Rle: L R→L R→Prop.
 axiom Rge: L R→L R→Prop.
 
 interpretation "real plus" 'plus x y =
- (cic:/matita/test/decl/Rplus.con x y).
+ (cic:/matita/tests/decl/Rplus.con x y).
 
 interpretation "real leq" 'leq x y =
- (cic:/matita/test/decl/Rle.con x y).
+ (cic:/matita/tests/decl/Rle.con x y).
 
 interpretation "real geq" 'geq x y =
- (cic:/matita/test/decl/Rge.con x y).
+ (cic:/matita/tests/decl/Rge.con x y).
 
 let rec elev (x:L R) (n:nat) on n: L R ≝
  match n with
@@ -81,7 +83,7 @@ let rec real_of_nat (n:nat) : L R ≝
   | S n ⇒ real_of_nat n + (j ? R1)
   ].
 
-coercion cic:/matita/test/decl/real_of_nat.con.
+coercion cic:/matita/tests/decl/real_of_nat.con.
 
 axiom Rplus_commutative: ∀x,y:R. (j ? x) + (j ? y) ≡ (j ? y) + (j ? x).
 axiom R0_neutral: ∀x:R. (j ? x) + (j ? R0) ≡ (j ? x).
@@ -114,4 +116,4 @@ axiom R2_1: (j ? R1) ≤ S (S O).
 axiom Rdiv_pos: ∀ x,y:R.
  (j ? R0) ≤ (j ? x) → (j ? R1) ≤ (j ? y) → (j ? R0) ≤ Rdiv (j ? x) (j ? y).
 axiom Rle_R0_R1: (j ? R0) ≤ (j ? R1).
-axiom div: ∀x:R. (j ? x) = Rdiv (j ? x) (S (S O)) → (j ? x) = O.
\ No newline at end of file
+axiom div: ∀x:R. (j ? x) = Rdiv (j ? x) (S (S O)) → (j ? x) = O.