From: Irene Schena Date: Fri, 17 Nov 2000 09:54:43 +0000 (+0000) Subject: Modified Files: X-Git-Tag: nogzip~174 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=ef35bce6975cc94557ecdce77a2d7fb4dd8adb4c Modified Files: 1) mml2mmlv1_0.xsl: added comments beginning with "HELM:" to the last modifications 2) rootcontent.xsl: updated comments 3) roottheory.xsl: ready to be the starting stylesheet for theory files in place of theory_content.xsl 4) theory_pres.xsl: "import" in place of "include" for annotated_pres.xsl Removed Files: annotatedcont.xsl.csc content.xsl.csc content_senza_tipi.13.9.00.xsl mml2mmlv1_0_original.xsl mmlextension_andrea.xsl mmlextension_irene.xsl objcontent.xsl.csc objcontent_old.xsl proof31-10-00.xsl rootcontent_withproofs.xsl style_prima_del_linguaggio_naturale/annotatedcont.xsl.csc style_prima_del_linguaggio_naturale/content.xsl.csc style_prima_del_linguaggio_naturale/mmlextension_andrea.xsl style_prima_del_linguaggio_naturale/mmlextension_irene.xsl style_prima_del_linguaggio_naturale/objcontent.xsl.csc style_prima_del_linguaggio_naturale/objcontent_old.xsl style_prima_del_linguaggio_naturale/rootcontent_withproofs.xsl --- diff --git a/helm/style/annotatedcont.xsl.csc b/helm/style/annotatedcont.xsl.csc deleted file mode 100644 index 3508d6be4..000000000 --- a/helm/style/annotatedcont.xsl.csc +++ /dev/null @@ -1,66 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/content.xsl.csc b/helm/style/content.xsl.csc deleted file mode 100644 index 5f7c1e131..000000000 --- a/helm/style/content.xsl.csc +++ /dev/null @@ -1,258 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - -http://localhost:8081/get?url= - - - - - - - - - [[]] - - - - - - - - - - - - - - - - - - - - arrow - - - - - - prod - - - [[]] - - - - - - - - - - - - - - - - - - - - cast - - - - - - - - - - - - - [[]] - - - - - - - - - - - - - - - - - app - - - - - - - - - - - - [[]] - - - - - - - - [[]] - - - - - - - - [[]] - - - - - - - - - - - - [[]] - - - - - - - - - - [[]] - - - - - - - - - - mutcase - - - - - - - - - - - - - - - - - - - app - - - - LAMBDA - - - - LAMBDA - - - - - - - - - fix - - - - - - - - - cofix - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/content_senza_tipi.13.9.00.xsl b/helm/style/content_senza_tipi.13.9.00.xsl deleted file mode 100644 index 7de998720..000000000 --- a/helm/style/content_senza_tipi.13.9.00.xsl +++ /dev/null @@ -1,215 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - -http://localhost:8081/get?url= - - - - - - - - - - - - - - - - - - - - - - arrow - - - - prod - - - - - - - - - - - - - - - - - cast - - - - - - - - - - - - - - - - - - - - - app - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - mutcase - - - - - - - - - - - - - - - app - - - - LAMBDA - - - - LAMBDA - - - - - - - - fix - - - - - - - - - cofix - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/mml2mmlv1_0.xsl b/helm/style/mml2mmlv1_0.xsl index 67e1accfb..330da7a24 100644 --- a/helm/style/mml2mmlv1_0.xsl +++ b/helm/style/mml2mmlv1_0.xsl @@ -20,6 +20,17 @@ + + + + + + + + + + + - + @@ -90,7 +101,7 @@ - + @@ -104,7 +115,7 @@ - + @@ -408,7 +419,7 @@ - @@ -903,7 +914,7 @@ - + * @@ -916,7 +927,7 @@ - + @@ -1955,3 +1966,19 @@ + + + + + + + + + + + + + + + + diff --git a/helm/style/mml2mmlv1_0_original.xsl b/helm/style/mml2mmlv1_0_original.xsl deleted file mode 100644 index 44c34df74..000000000 --- a/helm/style/mml2mmlv1_0_original.xsl +++ /dev/null @@ -1,1848 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - i - - - - - - - - - - - - - + - - - - i - - - - - - - - / - - - - - - - - / - - - - - - - - Polar - - - - - - - - - - Polar - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ln - - - exp - - - arcsin - - - arccos - - - arctan - - - arcsec - - - arccsc - - - arccot - - - arcsinh - - - arccosh - - - arctanh - - - arcsech - - - arccsch - - - arccoth - - - sin - - - cos - - - tan - - - - - - -1 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - Λ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - id - - - - - - - - - - - / - - - - - - - - - - e - - - - - - - - - - - ! - - - - - - - - - max - - - min - - - - - - - - - - - | - - - - - - - - - - - - - - max - - - min - - - - - - - - - | - - - - - - - max - - - min - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - % - - - / - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 2 - - - - - - - - gcd - - - - gcd - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - not - - - - - - - - - for all - - - - - - - : - - , - - - - - - - - - - - - - - - , - - - : - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - arg - - - Real - - - Imaginary - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - = - - - > - - - < - - - - - - - - - - - - - - - - - - - - - - - - - ln - - - - - ln - - - - - - - - - - - - - - - log - - - - - - log - - - - - - - - log - - - - log - - - - - - - - - - - - - - - - - - - - - - - - d - - - - d - - - - - - - - - - d - - d - - - - - - - - - - - - - - - d - - - - d - - - - - - - - - - d - - d - - - - - - - - - - - - - - - - - div - - - grad - - - curl - - - - - - - - - - - - - - - - - - Δ - 2 - - - - - - - - - - - - - | - - - - - - - - - | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - \ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - = - - - - - - - - - - - - - - - - - - - - - - - - - - lim - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - sin - - - cos - - - tan - - - sec - - - csc - - - cot - - - sinh - - - cosh - - - tanh - - - sech - - - csch - - - coth - - - arcsin - - - arccos - - - arctan - - - - - - - - - - - - - - - - - - σ - - - - - - - - - - - σ - - - - - - - 2 - - - - - - - median - - - - - - - - - - - mode - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - det - - - - - - - - T - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - . - - - - - - - diff --git a/helm/style/mmlextension_andrea.xsl b/helm/style/mmlextension_andrea.xsl deleted file mode 100644 index b4bbcdbdb..000000000 --- a/helm/style/mmlextension_andrea.xsl +++ /dev/null @@ -1,1052 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - type="text/xhtml" - - - - - - - - - - - - DEFINITION () OF TYPE - - - - - - - __ - - - - - - - - AS - - - - - - - __ - - - - - - - - - - - - - - - - - AXIOM () OF TYPE - - - - - - - __ - - - - - - - - - - - - - - - - - UNFINISHED PROOF () - - - - - - - THESIS: - - - - - - - __ - - - - - - - - CONJECTURES: - - - - - - - - __ - : - - - - - - - - - CORRESPONDING PROOF: - - - - - - - __ - - - - - - - - - - - - - - - - - - - - - - INDUCTIVE DEFINITION - - - COINDUCTIVE DEFINITION - - - - - AND - - - _ - () - - - - - - - __ - [ - - - - - - - - - : - - - - - - - - - ] - - - - - - - ] - - - - - - - - - OF ARITY - - - - - - - __ - - - - - - - - BUILT FROM - - - - - - - - - - __ - - - | - _ - - - OF - _ - - - - - - - - - - - - - - - - - - - VARIABLE OF TYPE - - - - - - - __ - - - - - - - - - - - - - - - - - - - - - - - - - : - - - - - - - - - - - - : - - - - - - - - - - - - - - - - - - - - - - - - - - - - Π - - - - - - - . - - - - - - - - Π - - : - - . - - - - - - - - - - - - ( - - - - - - - - → - - - - - - - - ) - - - - - - - ( - - → - - ) - - - - - - - - - - - ( - - - - - - - - - ( - - - - - - - - - ) - - - - - - - ( - - - _ - - - ) - - - - - - - - - - - ( - - - - - - - - :> - - - - - - - - ) - - - - - - - ( - - :> - - ) - - - - - Prop - - - Set - - - Type - - - - - - - - - - < - - - > - CASES - _ - - - - - - - - - - > - CASES - _ - - - - - - - - - OF - - - - - - - - - - - | - - - | - - - _ - - - ⇒ - - - - - - - - - - |_ - ⇒ - - - - - - - - - - END - - - - - - - <> - CASES - _ - - _ - OF - - - - | - - - - ⇒ - - - _ - END - - - - - - - - - - - FIX - _ - - { - - - - - - - __ - - - - - - - - : - - - - - - - - - - - := - - - - - - - - - := - - - - - - - - - - - - - } - - - - - - - FIX - - { - - - - - - - : - - := - - - } - - - - - - - - - - - - - - - - - COFIX - _ - - { - - - - - - - __ - - - - - - - - : - - - - - - - - - - - := - - - - - - - - - := - - - - - - - - - - - - - } - - - - - - - COFIX - - { - - - - - - - : - - := - - - } - - - - - - - - - - - - - - - - - - - - - - - - λ - - - - - - - . - - - - - - - - λ - - : - - . - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ( - - - - - - - - __ - - - - - - - - - - - ) - - - - - - - - - - - - - - - - - - - - - - { - - - - - - __ - | - - - - - - } - - - - - - - - - { - - - , - - - - - - - _ - - - , - - - - - - - } - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - > - - - - - - - - diff --git a/helm/style/mmlextension_irene.xsl b/helm/style/mmlextension_irene.xsl deleted file mode 100644 index 90852b79e..000000000 --- a/helm/style/mmlextension_irene.xsl +++ /dev/null @@ -1,868 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - DEFINITION () OF TYPE - - - - - - - __ - - - - - - - - AS - - - - - - - __ - - - - - - - - - - - - - - - - - AXIOM () OF TYPE - - - - - - - __ - - - - - - - - - - - - - - - - - UNFINISHED PROOF () - - - - - - - THESIS: - - - - - - - __ - - - - - - - - CONJECTURES: - - - - - - - - __ - : - - - - - - - - - CORRESPONDING PROOF: - - - - - - - __ - - - - - - - - - - - - - - - - - - - - - - INDUCTIVE DEFINITION - - - COINDUCTIVE DEFINITION - - - - - AND - - - _ - () - - - - - - - __ - [ - - - - - - - - - : - - - - - - - - - ] - - - - - - - ] - - - - - - - - - OF ARITY - - - - - - - __ - - - - - - - - BUILT FROM - - - - - - - - - - __ - - - | - _ - - - OF - _ - - - - - - - - - - - - - - - - - - - VARIABLE OF TYPE - - - - - - - __ - - - - - - - - - - - - - - - - - - - - - - - - - - - - Π - - : - - - - - - - - - - - . - - - - - - - - - . - - - - - - - - Π - - : - - . - - - - - - - - - - - - ( - - - - - - - - → - - - - - - - - ) - - - - - - - ( - - → - - ) - - - - - - - - - - - ( - - - - - - - - - ( - - - - - - - - - ) - - - - - - - ( - - - _ - - - ) - - - - - - - - - - - ( - - - - - - - - :> - - - - - - - - ) - - - - - - - ( - - :> - - ) - - - - - Prop - - - Set - - - Type - - - - - - - - - - < - - - > - CASES - _ - - - - - - - - - - > - CASES - _ - - - - - - - - - OF - - - - - - - - - - - | - - - | - - - _ - - - ⇒ - - - - - - - - - - |_ - ⇒ - - - - - - - - - - END - - - - - - - <> - CASES - _ - - _ - OF - - - - | - - - - ⇒ - - - _ - END - - - - - - - - - - - FIX - _ - - { - - - - - - - __ - - - - - - - - : - - - - - - - - - - - := - - - - - - - - - := - - - - - - - - - - - - - } - - - - - - - FIX - - { - - - - - - - : - - := - - - } - - - - - - - - - - - - - - - - - COFIX - _ - - { - - - - - - - __ - - - - - - - - : - - - - - - - - - - - := - - - - - - - - - := - - - - - - - - - - - - - } - - - - - - - COFIX - - { - - - - - - - : - - := - - - } - - - - - - - - - - - - - - - - - - - - - - - - - - λ - - - : - - - - - - - - - - - . - - - - - - - - - . - - - - - - - - λ - - : - - . - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - > - - - - - - - - diff --git a/helm/style/objcontent.xsl.csc b/helm/style/objcontent.xsl.csc deleted file mode 100644 index d2a846cba..000000000 --- a/helm/style/objcontent.xsl.csc +++ /dev/null @@ -1,223 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - type="text/xml" - href="" type="text/xsl" - type="xslt" - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -PROD - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - app - - - - - - - - - - - - - - - - - - - - - - - - - - $ - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/objcontent_old.xsl b/helm/style/objcontent_old.xsl deleted file mode 100644 index d3514b499..000000000 --- a/helm/style/objcontent_old.xsl +++ /dev/null @@ -1,220 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - type="text/xml" - href="" type="text/xsl" - type="xslt" - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -PROD - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - app - - - - - - - - - - - - - - - - - - - - - - - - - - $ - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/proof31-10-00.xsl b/helm/style/proof31-10-00.xsl deleted file mode 100644 index 3c4234307..000000000 --- a/helm/style/proof31-10-00.xsl +++ /dev/null @@ -1,210 +0,0 @@ - - - - - - - - - - - - - - -http://localhost:8081/get?url= - - - - - - - - - - - - - - - - - - rewrite - - - rw_step - - - - - - - - - - - and_ind - - - - - - - - - - - or_ind - - - - - - - - - proof - - - - - - - - - - - - - - - - - - - - - - - - - rw_step - - - - - - - - - - - - - - - - - - - - - - - - - - rewrite_and_apply - - rw_step - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - app - - - - - - - - - - - app - - * - * - * - - - - - - app - - - - - - - - - - - - - - diff --git a/helm/style/rootcontent.xsl b/helm/style/rootcontent.xsl index 7776afbbf..e82a13d63 100644 --- a/helm/style/rootcontent.xsl +++ b/helm/style/rootcontent.xsl @@ -7,11 +7,11 @@ - - + + - + diff --git a/helm/style/rootcontent_withproofs.xsl b/helm/style/rootcontent_withproofs.xsl deleted file mode 100644 index 11d668436..000000000 --- a/helm/style/rootcontent_withproofs.xsl +++ /dev/null @@ -1,29 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/roottheory.xsl b/helm/style/roottheory.xsl index d293ee6f2..5ba277e8d 100644 --- a/helm/style/roottheory.xsl +++ b/helm/style/roottheory.xsl @@ -4,19 +4,22 @@ + - - - - - + + + - - - + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/annotatedcont.xsl.csc b/helm/style/style_prima_del_linguaggio_naturale/annotatedcont.xsl.csc deleted file mode 100644 index 3508d6be4..000000000 --- a/helm/style/style_prima_del_linguaggio_naturale/annotatedcont.xsl.csc +++ /dev/null @@ -1,66 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/style_prima_del_linguaggio_naturale/content.xsl.csc b/helm/style/style_prima_del_linguaggio_naturale/content.xsl.csc deleted file mode 100644 index 5f7c1e131..000000000 --- a/helm/style/style_prima_del_linguaggio_naturale/content.xsl.csc +++ /dev/null @@ -1,258 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - -http://localhost:8081/get?url= - - - - - - - - - [[]] - - - - - - - - - - - - - - - - - - - - arrow - - - - - - prod - - - [[]] - - - - - - - - - - - - - - - - - - - - cast - - - - - - - - - - - - - [[]] - - - - - - - - - - - - - - - - - app - - - - - - - - - - - - [[]] - - - - - - - - [[]] - - - - - - - - [[]] - - - - - - - - - - - - [[]] - - - - - - - - - - [[]] - - - - - - - - - - mutcase - - - - - - - - - - - - - - - - - - - app - - - - LAMBDA - - - - LAMBDA - - - - - - - - - fix - - - - - - - - - cofix - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/style_prima_del_linguaggio_naturale/mmlextension_andrea.xsl b/helm/style/style_prima_del_linguaggio_naturale/mmlextension_andrea.xsl deleted file mode 100644 index e75affee9..000000000 --- a/helm/style/style_prima_del_linguaggio_naturale/mmlextension_andrea.xsl +++ /dev/null @@ -1,1052 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - type="text/xhtml" - - - - - - - - - - - - DEFINITION () OF TYPE - - - - - - - __ - - - - - - - - AS - - - - - - - __ - - - - - - - - - - - - - - - - - AXIOM () OF TYPE - - - - - - - __ - - - - - - - - - - - - - - - - - UNFINISHED PROOF () - - - - - - - THESIS: - - - - - - - __ - - - - - - - - CONJECTURES: - - - - - - - - __ - : - - - - - - - - - CORRESPONDING PROOF: - - - - - - - __ - - - - - - - - - - - - - - - - - - - - - - INDUCTIVE DEFINITION - - - COINDUCTIVE DEFINITION - - - - - AND - - - _ - () - - - - - - - __ - [ - - - - - - - - - : - - - - - - - - - ] - - - - - - - ] - - - - - - - - - OF ARITY - - - - - - - __ - - - - - - - - BUILT FROM - - - - - - - - - - __ - - - | - _ - - - OF - _ - - - - - - - - - - - - - - - - - - - VARIABLE OF TYPE - - - - - - - __ - - - - - - - - - - - - - - - - - - - - - - - - - : - - - - - - - - - - - - : - - - - - - - - - - - - - - - - - - - - - - - - - - - - Π - - - - - - - . - - - - - - - - Π - - : - - . - - - - - - - - - - - - ( - - - - - - - - → - - - - - - - - ) - - - - - - - ( - - → - - ) - - - - - - - - - - - ( - - - - - - - - - ( - - - - - - - - - ) - - - - - - - ( - - - _ - - - ) - - - - - - - - - - - ( - - - - - - - - :> - - - - - - - - ) - - - - - - - ( - - :> - - ) - - - - - Prop - - - Set - - - Type - - - - - - - - - - < - - - > - CASES - _ - - - - - - - - - - > - CASES - _ - - - - - - - - - OF - - - - - - - - - - - | - - - | - - - _ - - - ⇒ - - - - - - - - - - |_ - ⇒ - - - - - - - - - - END - - - - - - - <> - CASES - _ - - _ - OF - - - - | - - - - ⇒ - - - _ - END - - - - - - - - - - - FIX - _ - - { - - - - - - - __ - - - - - - - - : - - - - - - - - - - - := - - - - - - - - - := - - - - - - - - - - - - - } - - - - - - - FIX - - { - - - - - - - : - - := - - - } - - - - - - - - - - - - - - - - - COFIX - _ - - { - - - - - - - __ - - - - - - - - : - - - - - - - - - - - := - - - - - - - - - := - - - - - - - - - - - - - } - - - - - - - COFIX - - { - - - - - - - : - - := - - - } - - - - - - - - - - - - - - - - - - - - - - - - λ - - - - - - - . - - - - - - - - λ - - : - - . - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ( - - - - - - - - __ - - - - - - - - - - - ) - - - - - - - - - - - - - - - - - - - - - - { - - - - - - __ - | - - - - - - } - - - - - - - - - { - - - , - - - - - - - _ - - - , - - - - - - - } - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - > - - - - - - - - diff --git a/helm/style/style_prima_del_linguaggio_naturale/mmlextension_irene.xsl b/helm/style/style_prima_del_linguaggio_naturale/mmlextension_irene.xsl deleted file mode 100644 index dfe2e6aa3..000000000 --- a/helm/style/style_prima_del_linguaggio_naturale/mmlextension_irene.xsl +++ /dev/null @@ -1,868 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - DEFINITION () OF TYPE - - - - - - - __ - - - - - - - - AS - - - - - - - __ - - - - - - - - - - - - - - - - - AXIOM () OF TYPE - - - - - - - __ - - - - - - - - - - - - - - - - - UNFINISHED PROOF () - - - - - - - THESIS: - - - - - - - __ - - - - - - - - CONJECTURES: - - - - - - - - __ - : - - - - - - - - - CORRESPONDING PROOF: - - - - - - - __ - - - - - - - - - - - - - - - - - - - - - - INDUCTIVE DEFINITION - - - COINDUCTIVE DEFINITION - - - - - AND - - - _ - () - - - - - - - __ - [ - - - - - - - - - : - - - - - - - - - ] - - - - - - - ] - - - - - - - - - OF ARITY - - - - - - - __ - - - - - - - - BUILT FROM - - - - - - - - - - __ - - - | - _ - - - OF - _ - - - - - - - - - - - - - - - - - - - VARIABLE OF TYPE - - - - - - - __ - - - - - - - - - - - - - - - - - - - - - - - - - - - - Π - - : - - - - - - - - - - - . - - - - - - - - - . - - - - - - - - Π - - : - - . - - - - - - - - - - - - ( - - - - - - - - → - - - - - - - - ) - - - - - - - ( - - → - - ) - - - - - - - - - - - ( - - - - - - - - - ( - - - - - - - - - ) - - - - - - - ( - - - _ - - - ) - - - - - - - - - - - ( - - - - - - - - :> - - - - - - - - ) - - - - - - - ( - - :> - - ) - - - - - Prop - - - Set - - - Type - - - - - - - - - - < - - - > - CASES - _ - - - - - - - - - - > - CASES - _ - - - - - - - - - OF - - - - - - - - - - - | - - - | - - - _ - - - ⇒ - - - - - - - - - - |_ - ⇒ - - - - - - - - - - END - - - - - - - <> - CASES - _ - - _ - OF - - - - | - - - - ⇒ - - - _ - END - - - - - - - - - - - FIX - _ - - { - - - - - - - __ - - - - - - - - : - - - - - - - - - - - := - - - - - - - - - := - - - - - - - - - - - - - } - - - - - - - FIX - - { - - - - - - - : - - := - - - } - - - - - - - - - - - - - - - - - COFIX - _ - - { - - - - - - - __ - - - - - - - - : - - - - - - - - - - - := - - - - - - - - - := - - - - - - - - - - - - - } - - - - - - - COFIX - - { - - - - - - - : - - := - - - } - - - - - - - - - - - - - - - - - - - - - - - - - - λ - - - : - - - - - - - - - - - . - - - - - - - - - . - - - - - - - - λ - - : - - . - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - > - - - - - - - - diff --git a/helm/style/style_prima_del_linguaggio_naturale/objcontent.xsl.csc b/helm/style/style_prima_del_linguaggio_naturale/objcontent.xsl.csc deleted file mode 100644 index d2a846cba..000000000 --- a/helm/style/style_prima_del_linguaggio_naturale/objcontent.xsl.csc +++ /dev/null @@ -1,223 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - type="text/xml" - href="" type="text/xsl" - type="xslt" - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -PROD - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - app - - - - - - - - - - - - - - - - - - - - - - - - - - $ - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/style_prima_del_linguaggio_naturale/objcontent_old.xsl b/helm/style/style_prima_del_linguaggio_naturale/objcontent_old.xsl deleted file mode 100644 index d3514b499..000000000 --- a/helm/style/style_prima_del_linguaggio_naturale/objcontent_old.xsl +++ /dev/null @@ -1,220 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - type="text/xml" - href="" type="text/xsl" - type="xslt" - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -PROD - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - app - - - - - - - - - - - - - - - - - - - - - - - - - - $ - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/style_prima_del_linguaggio_naturale/rootcontent_withproofs.xsl b/helm/style/style_prima_del_linguaggio_naturale/rootcontent_withproofs.xsl deleted file mode 100644 index 11d668436..000000000 --- a/helm/style/style_prima_del_linguaggio_naturale/rootcontent_withproofs.xsl +++ /dev/null @@ -1,29 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/theory_pres.xsl b/helm/style/theory_pres.xsl index 9a96cdc03..f8ade2a82 100644 --- a/helm/style/theory_pres.xsl +++ b/helm/style/theory_pres.xsl @@ -3,12 +3,13 @@ + - +