From: Irene Schena Date: Mon, 15 Apr 2002 16:17:20 +0000 (+0000) Subject: Modified Files: X-Git-Tag: V_0_3_0_debian_8~160 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=c8c75f895d51cfbc257260859653a68f74117179 Modified Files: 1) mmlnotation.xsl xslt_index.txt: MathML default presentation now is generated by mmlctop.xsl Added Files: 1) mmlctop.xsl mmlctop2_0.xsl: link and new Igor stylesheet for MathML default presentation --- diff --git a/helm/style/mmlctop.xsl b/helm/style/mmlctop.xsl new file mode 100644 index 000000000..0a0e454d9 --- /dev/null +++ b/helm/style/mmlctop.xsl @@ -0,0 +1,3982 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ⁢ + e + ⁢ + + + + + + + - + + + + + + + + ⁢ + i + + + + + + + + - + + + + + + + + ⁢ + i + + + + + + + + + + + + + + + + + + + + + + + + Polar + ⁢ + + + + + + + + + + Polar + ⁢ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + ⁢ + i + + + + + + + + - + + + + + + + + ⁢ + i + + + + + + + + + + + + + + + + + + + + + + + + Polar + ⁢ + + + + + + + + + + Polar + ⁢ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ⁡ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ⁡ + + + + + + + + + ⁡ + + + + + + + + + + + + + + + + + + + + + + + + + + + [ + + + ] + + + + + + + + + + + + + + ⁡ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + -1 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Λ + ⁡ + + + + + + + + + + + + + + + + + + + + + + + + + + ⁡ + + + + + + + + + + + + + + + + + + + + + + ∘ + + + + + + + + + id + + + id + + + + + + + + + + + + + { + + + + + + + + + + + + if + + + + + + + + + + + + + + + otherwise + + + + + + + + + + + + + + + + + + domain + + + + + + + + + + + + + + + codomain + + + + + + + + + + + + + + + image + + + + + + + + + + + + + + + + + + ⌊ + + + + + + + + + + + + + + + + + + + + + + ⌊ + + + + + + + + + + + + + + + + + + e + + + + + + + + + + + + + + + + + + + + + + ! + + + + + + + + + + + + + + + + + + + + max + + + + + + + + + min + + + + + + + + + + + | + + + + + + + + + + + + + + + + + + + + max + + + + + + + + + min + + + + + + + + + | + + + + + + + + + + + + + max + + + + + + + + + min + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + * + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 2 + + + + + + + + + + + + + + + + + + + gcd + + + + + + + + + + gcd + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ∧ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ∨ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ⊻ + + + + + + + + + + + + + + + + + + + + + + + ¬ + + + + + + + + + + + + + + + + + + + + for all + + + + + + + + + + + + : + + , + + + + + + + + + + + + + + + + + + + ∃ + + + + + + + + + + + + , + + + + : + + + + + + + + + + + + + + + + + + + + + + | + + + + + + + + | + + + + + + + + + + + + + + + + + + + | + + + + + + + + | + + + + + + + + + + + + + + + + + + + + + + + + ̲ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + lcm + + + + + + + + + + lcm + + + + + + + + + + + + + + + + + + + + + + + + + + + + ⌊ + + + + + + + + + + +⌋ + + + + + + + + + + + + + + + + + + + + + ⌈ + + + + + + + + + + + ⌉ + + + + + + + + + + + + + + + + + + + + + + + + + ≠ + + + + + + + + + ≊ + + + + + + + + + | + + + + + + + + + → + + + + + + + + + ⇒ + + + + + + + + + ∈ + + + + + + + + + ∉ + + + + + + + + + ⊄ + + + + + + + + + ⊈ + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + ⊆ + + + + + + + + + ⊂ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ≥ + + + + + + + + + ≤ + + + + + + + + + ≡ + + + + + + + + + + + + + + + + + + + + + + + + + + + + ln + + + + + + + + + + + ln + + + ⁡ + + + + + + + + + + + + + + + + + + + + + + + + log + + + + + + + + + + + + log + + + + + + + + + + + + + + log + + + + + + + + + + log + + + + + + ⁡ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + d + + + + d + + + + + + + + + + + + + + + + d + + d + + + + + + + + + + + + + + + + + + + + + + + + + + d + + + + d + + + + + + + + + + + + + + + + d + + d + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Δ + 2 + + + + + + + + + + + + + + + + + + | + + + + + + + + + | + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ⋃ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ⋂ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + \ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + × + + + + + + + + + + + + + + + + + + + + + + + + + | + + + + + + + + + + | + + + + + + + + + + + + + + + + + + + + + + + + + + ∑ + + + + + + + + + ∏ + + + + + = + + + + + + + + + + + ∑ + + + ∏ + + + + + + + + + + + + + + + + + + ∑ + + + + + + + + + + ∏ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ∫ + + + + + + + d + + + + + + + + + + + + + + ∫ + + + + + + + + + + + + + + + + + + + ∫ + + + + + d + + + + + + + + + + + + + ∫ + + + + + d + + + + + + + + + + + ∫ + + d + + + + + + + + + + + + + + + + + + + + + + lim + + + + → + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ⁡ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + < + + + + , + + + + + + + + + + > + + + + + + + + + + + + + + + + + + + σ + + + + + + + + + + + + + + + + + + + + + + + σ + + + + + + + 2 + + + + + + + + + + + + + + + + + + median + + + + + + + + + + + + + + + + + + + + + + mode + + + + + + + + + + + + + + + + + + + + + + + + < + + + + + + + + + + + + + + + + + + + + + + + + + + + + + > + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + det + + + + + + + + + + + + + + + + + + + T + + + + + + + + + + + + + + + + + + + + + + + + + + * + + + + + + + + + + + + + + + + + + + + + + + + + + ⨯ + + + + + + + + + + + + + + + + + + + + + + + + + + + ℤ + + + + + + + + + + + ℝ + + + + + + + + + + + ℚ + + + + + + + + + + + ℕ + + + + + + + + + + + ℂ + + + + + + + + + + + ℙ + + + + + + + + + + + ⅇ + + + + + + + + + + + + + + + + + + + + + + NaN + + + + + + + + + + true + + + + + + + + + + false + + + + + + + + + + + + + + + + + + + + + + + + π + + + + + + + + + + + + γ + + + + + + + + + + + + ∞ + + + + + diff --git a/helm/style/mmlctop2_0.xsl b/helm/style/mmlctop2_0.xsl new file mode 100644 index 000000000..0a0e454d9 --- /dev/null +++ b/helm/style/mmlctop2_0.xsl @@ -0,0 +1,3982 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ⁢ + e + ⁢ + + + + + + + - + + + + + + + + ⁢ + i + + + + + + + + - + + + + + + + + ⁢ + i + + + + + + + + + + + + + + + + + + + + + + + + Polar + ⁢ + + + + + + + + + + Polar + ⁢ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + ⁢ + i + + + + + + + + - + + + + + + + + ⁢ + i + + + + + + + + + + + + + + + + + + + + + + + + Polar + ⁢ + + + + + + + + + + Polar + ⁢ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ⁡ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ⁡ + + + + + + + + + ⁡ + + + + + + + + + + + + + + + + + + + + + + + + + + + [ + + + ] + + + + + + + + + + + + + + ⁡ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + -1 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Λ + ⁡ + + + + + + + + + + + + + + + + + + + + + + + + + + ⁡ + + + + + + + + + + + + + + + + + + + + + + ∘ + + + + + + + + + id + + + id + + + + + + + + + + + + + { + + + + + + + + + + + + if + + + + + + + + + + + + + + + otherwise + + + + + + + + + + + + + + + + + + domain + + + + + + + + + + + + + + + codomain + + + + + + + + + + + + + + + image + + + + + + + + + + + + + + + + + + ⌊ + + + + + + + + + + + + + + + + + + + + + + ⌊ + + + + + + + + + + + + + + + + + + e + + + + + + + + + + + + + + + + + + + + + + ! + + + + + + + + + + + + + + + + + + + + max + + + + + + + + + min + + + + + + + + + + + | + + + + + + + + + + + + + + + + + + + + max + + + + + + + + + min + + + + + + + + + | + + + + + + + + + + + + + max + + + + + + + + + min + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + * + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 2 + + + + + + + + + + + + + + + + + + + gcd + + + + + + + + + + gcd + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ∧ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ∨ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ⊻ + + + + + + + + + + + + + + + + + + + + + + + ¬ + + + + + + + + + + + + + + + + + + + + for all + + + + + + + + + + + + : + + , + + + + + + + + + + + + + + + + + + + ∃ + + + + + + + + + + + + , + + + + : + + + + + + + + + + + + + + + + + + + + + + | + + + + + + + + | + + + + + + + + + + + + + + + + + + + | + + + + + + + + | + + + + + + + + + + + + + + + + + + + + + + + + ̲ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + lcm + + + + + + + + + + lcm + + + + + + + + + + + + + + + + + + + + + + + + + + + + ⌊ + + + + + + + + + + +⌋ + + + + + + + + + + + + + + + + + + + + + ⌈ + + + + + + + + + + + ⌉ + + + + + + + + + + + + + + + + + + + + + + + + + ≠ + + + + + + + + + ≊ + + + + + + + + + | + + + + + + + + + → + + + + + + + + + ⇒ + + + + + + + + + ∈ + + + + + + + + + ∉ + + + + + + + + + ⊄ + + + + + + + + + ⊈ + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + ⊆ + + + + + + + + + ⊂ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ≥ + + + + + + + + + ≤ + + + + + + + + + ≡ + + + + + + + + + + + + + + + + + + + + + + + + + + + + ln + + + + + + + + + + + ln + + + ⁡ + + + + + + + + + + + + + + + + + + + + + + + + log + + + + + + + + + + + + log + + + + + + + + + + + + + + log + + + + + + + + + + log + + + + + + ⁡ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + d + + + + d + + + + + + + + + + + + + + + + d + + d + + + + + + + + + + + + + + + + + + + + + + + + + + d + + + + d + + + + + + + + + + + + + + + + d + + d + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Δ + 2 + + + + + + + + + + + + + + + + + + | + + + + + + + + + | + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ⋃ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ⋂ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + \ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + × + + + + + + + + + + + + + + + + + + + + + + + + + | + + + + + + + + + + | + + + + + + + + + + + + + + + + + + + + + + + + + + ∑ + + + + + + + + + ∏ + + + + + = + + + + + + + + + + + ∑ + + + ∏ + + + + + + + + + + + + + + + + + + ∑ + + + + + + + + + + ∏ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ∫ + + + + + + + d + + + + + + + + + + + + + + ∫ + + + + + + + + + + + + + + + + + + + ∫ + + + + + d + + + + + + + + + + + + + ∫ + + + + + d + + + + + + + + + + + ∫ + + d + + + + + + + + + + + + + + + + + + + + + + lim + + + + → + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ⁡ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + < + + + + , + + + + + + + + + + > + + + + + + + + + + + + + + + + + + + σ + + + + + + + + + + + + + + + + + + + + + + + σ + + + + + + + 2 + + + + + + + + + + + + + + + + + + median + + + + + + + + + + + + + + + + + + + + + + mode + + + + + + + + + + + + + + + + + + + + + + + + < + + + + + + + + + + + + + + + + + + + + + + + + + + + + + > + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + det + + + + + + + + + + + + + + + + + + + T + + + + + + + + + + + + + + + + + + + + + + + + + + * + + + + + + + + + + + + + + + + + + + + + + + + + + ⨯ + + + + + + + + + + + + + + + + + + + + + + + + + + + ℤ + + + + + + + + + + + ℝ + + + + + + + + + + + ℚ + + + + + + + + + + + ℕ + + + + + + + + + + + ℂ + + + + + + + + + + + ℙ + + + + + + + + + + + ⅇ + + + + + + + + + + + + + + + + + + + + + + NaN + + + + + + + + + + true + + + + + + + + + + false + + + + + + + + + + + + + + + + + + + + + + + + π + + + + + + + + + + + + γ + + + + + + + + + + + + ∞ + + + + + diff --git a/helm/style/mmlnotation.xsl b/helm/style/mmlnotation.xsl index 3ebf23ba7..babc7f41d 100644 --- a/helm/style/mmlnotation.xsl +++ b/helm/style/mmlnotation.xsl @@ -36,7 +36,7 @@ - + diff --git a/helm/style/xslt_index.txt b/helm/style/xslt_index.txt index 8028625ce..f2e42135f 100644 --- a/helm/style/xslt_index.txt +++ b/helm/style/xslt_index.txt @@ -22,7 +22,7 @@ mk_dep_graph.xsl mk_meta_and_dep_graph.xsl mk_meta_graph.xsl mk_meta_theory.xsl -mmlctop.xsl-0.14 +mmlctop.xsl mmlextension.xsl mmlnotation.xsl mmltheoryextension.xsl