From: Claudio Sacerdoti Coen Date: Tue, 11 Jun 2002 10:19:54 +0000 (+0000) Subject: New: expected types (in the sense of Yann Coscoy) now availables for X-Git-Tag: V_0_3_0_debian_8~52 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a38dce333847f6a1eaed563f7a2260e1cfc1ff2e;p=helm.git New: expected types (in the sense of Yann Coscoy) now availables for MathML Content and MathML Presentation. HTML support is still missing (and bugs may have been introduced when expected types are present) --- diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl index 01b2a41cb..dc6d6d7a8 100644 --- a/helm/style/content_to_html.xsl +++ b/helm/style/content_to_html.xsl @@ -407,12 +407,13 @@ - +  proves  + letin1 (inline error) diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl index 6ab6ffe1f..d01670473 100644 --- a/helm/style/mmlextension.xsl +++ b/helm/style/mmlextension.xsl @@ -1124,7 +1124,9 @@ which generates the toplevel element (see for instance xlink) --> We can prove _ - + + + _ (explain) @@ -1145,23 +1147,40 @@ which generates the toplevel element (see for instance xlink) --> + + + + _ + + + (hide details) + + + we proved _ - - - _ - - - (hide details) - - + + + + + + + + that is equivalent to + _ + + + + + + @@ -1188,7 +1207,9 @@ which generates the toplevel element (see for instance xlink) --> We can prove _ - + + + _ (explain) @@ -1209,23 +1230,40 @@ which generates the toplevel element (see for instance xlink) --> + + + + _ + + + (hide details) + + + we proved _ - - - _ - - - (hide details) - - + + + + + + + + that is equivalent to + _ + + + + + + diff --git a/helm/style/objcontent.xsl b/helm/style/objcontent.xsl index b4a0e748d..ceb7a22ba 100644 --- a/helm/style/objcontent.xsl +++ b/helm/style/objcontent.xsl @@ -61,7 +61,7 @@ - + diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl index 5a34d8a06..1d619260a 100644 --- a/helm/style/proofs.xsl +++ b/helm/style/proofs.xsl @@ -597,7 +597,7 @@ full_or_ind + select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*[1]"/> left_case @@ -629,7 +629,7 @@ or_ind + select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*[1]"/>