]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/procedural/Coq/Reals/RiemannInt.mma
transcript: improved debuugging facilities
[helm.git] / helm / software / matita / contribs / procedural / Coq / Reals / RiemannInt.mma
index d4704676bde70ba800325017e5f86039e8683525..b032806c85f7050d199d4f077d695d2966d09056 100644 (file)
@@ -92,7 +92,7 @@ inline procedural "cic:/Coq/Reals/RiemannInt/RiemannInt_P5.con" as lemma.
 
 (*#*************************************)
 
-(* C°([a,b]) is included in L1([a,b]) *)
+(* C\176\([a,b]) is included in L1([a,b]) *)
 
 (*#*************************************)