transformation from automath to intermediate language started

[helm.git] / helm / software / matita / library / Q / frac.ma

diff --git a/helm/software/matita/library/Q/frac.ma b/helm/software/matita/library/Q/frac.ma
index a1f0cd54a2218c868ca5cefbf703a97ebd544190..e4a2fc566408232e58f32a1d6d3c5ef854bce93b 100644 (file)
--- a/helm/software/matita/library/Q/frac.ma
+++ b/helm/software/matita/library/Q/frac.ma
@@ -52,8 +52,6 @@ reflexivity.
 qed.
 *)
 
-Qtimes1 == Qtimes_numerator_denominator
-
 (*     
 definition numQ:Q \to Z \def
 \lambda q. 
@@ -83,7 +81,7 @@ elim r
   |elim f
     [reflexivity
     |reflexivity
-    |apply Qtimes1.
+    |apply Qtimes_numerator_denominator.
     ]
   ]
 qed.*)
@@ -101,7 +99,7 @@ elim r
   |elim f
     [reflexivity
     |reflexivity
-    |apply Qtimes1.
+    |apply Qtimes_numerator_denominator.
     ]
   ]
 qed.*)