]> matita.cs.unibo.it Git - helm.git/commitdiff
Added more typing information to remove a coercion.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sun, 5 Nov 2006 10:14:04 +0000 (10:14 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sun, 5 Nov 2006 10:14:04 +0000 (10:14 +0000)
helm/software/matita/dama/reals.ma

index dbd4fa01e26282460a1767a4c27532edded44afc..97ca4151fed9225137df2fd185aaeb219f06aa87 100644 (file)
@@ -121,4 +121,4 @@ definition max: ∀R:real.R → R → R.
  apply cauchy_max_seq.
 qed.
 
-definition abs \def λR.λx:Type_OF_real R. max R x (-x).
\ No newline at end of file
+definition abs \def λR:real.λx:R. max R x (-x).
\ No newline at end of file