From aabc65e7ce88b0a625e83449f1f8fceda3be393a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 31 Oct 2000 17:25:23 +0000 Subject: [PATCH] Added style before natural language synthesis --- .../annotatedcont.xsl | 73 + .../annotatedcont.xsl.csc | 66 + .../annotatedpres.xsl | 34 + .../basic.xsl | 253 +++ .../content.xsl | 215 ++ .../content.xsl.csc | 258 +++ .../content_to_html.xsl | 657 ++++++ .../html_init.xsl | 259 +++ .../html_reals.xsl | 234 ++ .../html_set.xsl | 463 ++++ .../mml2mmlv1_0.xsl | 1957 +++++++++++++++++ .../mml2mmlv1_0_original.xsl | 1848 ++++++++++++++++ .../mmlextension.xsl | 1128 ++++++++++ .../mmlextension_andrea.xsl | 1052 +++++++++ .../mmlextension_irene.xsl | 868 ++++++++ .../objcontent.xsl | 232 ++ .../objcontent.xsl.csc | 223 ++ .../objcontent_old.xsl | 220 ++ .../params.xsl | 191 ++ .../reals.xsl | 277 +++ .../ricerca.xsl | 91 + .../rootcontent.xsl | 29 + .../rootcontent_withproofs.xsl | 29 + .../roottheory.xsl | 22 + .../set.xsl | 487 ++++ .../theory_content.xsl | 57 + .../theory_pres.xsl | 34 + 27 files changed, 11257 insertions(+) create mode 100644 helm/style/style_prima_del_linguaggio_naturale/annotatedcont.xsl create mode 100644 helm/style/style_prima_del_linguaggio_naturale/annotatedcont.xsl.csc create mode 100644 helm/style/style_prima_del_linguaggio_naturale/annotatedpres.xsl create mode 100644 helm/style/style_prima_del_linguaggio_naturale/basic.xsl create mode 100644 helm/style/style_prima_del_linguaggio_naturale/content.xsl create mode 100644 helm/style/style_prima_del_linguaggio_naturale/content.xsl.csc create mode 100644 helm/style/style_prima_del_linguaggio_naturale/content_to_html.xsl create mode 100644 helm/style/style_prima_del_linguaggio_naturale/html_init.xsl create mode 100644 helm/style/style_prima_del_linguaggio_naturale/html_reals.xsl create mode 100644 helm/style/style_prima_del_linguaggio_naturale/html_set.xsl create mode 100644 helm/style/style_prima_del_linguaggio_naturale/mml2mmlv1_0.xsl create mode 100644 helm/style/style_prima_del_linguaggio_naturale/mml2mmlv1_0_original.xsl create mode 100644 helm/style/style_prima_del_linguaggio_naturale/mmlextension.xsl create mode 100644 helm/style/style_prima_del_linguaggio_naturale/mmlextension_andrea.xsl create mode 100644 helm/style/style_prima_del_linguaggio_naturale/mmlextension_irene.xsl create mode 100644 helm/style/style_prima_del_linguaggio_naturale/objcontent.xsl create mode 100644 helm/style/style_prima_del_linguaggio_naturale/objcontent.xsl.csc create mode 100644 helm/style/style_prima_del_linguaggio_naturale/objcontent_old.xsl create mode 100644 helm/style/style_prima_del_linguaggio_naturale/params.xsl create mode 100644 helm/style/style_prima_del_linguaggio_naturale/reals.xsl create mode 100644 helm/style/style_prima_del_linguaggio_naturale/ricerca.xsl create mode 100644 helm/style/style_prima_del_linguaggio_naturale/rootcontent.xsl create mode 100644 helm/style/style_prima_del_linguaggio_naturale/rootcontent_withproofs.xsl create mode 100644 helm/style/style_prima_del_linguaggio_naturale/roottheory.xsl create mode 100644 helm/style/style_prima_del_linguaggio_naturale/set.xsl create mode 100644 helm/style/style_prima_del_linguaggio_naturale/theory_content.xsl create mode 100644 helm/style/style_prima_del_linguaggio_naturale/theory_pres.xsl diff --git a/helm/style/style_prima_del_linguaggio_naturale/annotatedcont.xsl b/helm/style/style_prima_del_linguaggio_naturale/annotatedcont.xsl new file mode 100644 index 000000000..e97d08f2b --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/annotatedcont.xsl @@ -0,0 +1,73 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/annotatedcont.xsl.csc b/helm/style/style_prima_del_linguaggio_naturale/annotatedcont.xsl.csc new file mode 100644 index 000000000..3508d6be4 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/annotatedcont.xsl.csc @@ -0,0 +1,66 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/annotatedpres.xsl b/helm/style/style_prima_del_linguaggio_naturale/annotatedpres.xsl new file mode 100644 index 000000000..511f915f5 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/annotatedpres.xsl @@ -0,0 +1,34 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/basic.xsl b/helm/style/style_prima_del_linguaggio_naturale/basic.xsl new file mode 100644 index 000000000..3f5422a72 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/basic.xsl @@ -0,0 +1,253 @@ + + + + + + + + + + + + + + +http://localhost:8081/get?url= + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + $x + + + app + + $x + + + + + + + + + + + + + + + + + + + + + + + + + app + + + + + + + + + + + + + + + + app + + + + + + + + + x + + + + app + + x + + + + app + + x + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/content.xsl b/helm/style/style_prima_del_linguaggio_naturale/content.xsl new file mode 100644 index 000000000..7de998720 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/content.xsl @@ -0,0 +1,215 @@ + + + + + + + + + + + + + + + + + + + + + + +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/content.xsl.csc b/helm/style/style_prima_del_linguaggio_naturale/content.xsl.csc new file mode 100644 index 000000000..5f7c1e131 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/content.xsl.csc @@ -0,0 +1,258 @@ + + + + + + + + + + + + + + + + + + + + + + +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/content_to_html.xsl b/helm/style/style_prima_del_linguaggio_naturale/content_to_html.xsl new file mode 100644 index 000000000..dd1c07794 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/content_to_html.xsl @@ -0,0 +1,657 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +   + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + P + + : + + +
+ + + + . + + + + + + + P + + : + + . + + + + + + + + ( + + + +
+ + + + + ® + + + + ) + + + ( + + + ® + + ) + + + + + + + ( + + + + +
+ + + + + + + + ) + + + ( + + +   + + + ) + + + + + + + + + ( + + +
+ + + :> + + + + ) + + + ( + + :> + + ) + + + + + + + + + + + + Prop + + + Set + + + Type + + + + + < + + + + > + CASE + + + + OF + +
+ + + + + +    + + + | + + + + Þ + + + + + + + < + + > + CASE + + OF + + + + | + + + + Þ + + + + + + + + + + + FIX + + { + +
+ + + + + : + + + +
+ + + + := + + + + +
+ + + + } + + + FIX + + { + + + : + + := + + + + } + + + ; + + + + + + + + + + COFIX + + { +
+ + + + + + : + + + +
+ + + + := + + + + + +
+ + + + } + + + COFIX + + { + + + : + + := + + + + } + + + ; + + + + + + + + + + + + + + + + + + + + + + + l + + : + + +
+ + + + . + + + + + + + l + + : + + . + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

+DEFINITION ()
+TYPE =
+ + + + + +
+BODY =
+ + + + + + +

+ + + + + + +

+AXIOM ()
+TYPE = + + +

+ + + + + + +

+UNFINISHED PROOF ()
+THESIS: + +
+CONJECTURES: + +
+ + + + : + + + + +
+PROOF: + + + +

+ + + + + + +

+ + + + + + INDUCTIVE DEFINITION + + + COINDUCTIVE DEFINITION + + + + + AND + + + () + [ + + + + : + + + + ]
+ OF ARITY + + +
+ BUILT FROM: + +
+ + + + + +    + + + | + + + + : + + + + + +

+ + + + + + +

+VARIABLE
+TYPE = + + +

+ + + + + + + + + + +

BEGIN OF SECTION

+ +

END OF SECTION

+ + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/html_init.xsl b/helm/style/style_prima_del_linguaggio_naturale/html_init.xsl new file mode 100644 index 000000000..9e81b169c --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/html_init.xsl @@ -0,0 +1,259 @@ + + + + + + + + + +http://localhost:8081/get?url= + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + + + + + + + + ) + + + ( + + + + + + + + + + + ) + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + ( + + + +
+ + + + + + + + - + + + + + ) + + + ( + + + + + + - + + + ) + + + + + + + + + + + + + + + + + + + Ø + + + + + + + + + + + + + + + + + + + + + + $ + + + : + + + +
+ + + + . + + + + + + + + + + $ + + + : + + . + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/html_reals.xsl b/helm/style/style_prima_del_linguaggio_naturale/html_reals.xsl new file mode 100644 index 000000000..04ff478c5 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/html_reals.xsl @@ -0,0 +1,234 @@ + + + + + + + + + +http://localhost:8081/get?url= + + + + + + + + + + + + + + + + + + + lim + + + + ® + + +
+ + + + + + + + + + + + + lim + + + + ® + + + + + + + + + + + + + + + + + + + + + + d + / + + d + + + + + + + + + + + + + + + + | + + + + | + + + + + + + + + + + + + + ! + + + + + + + + + + + (sqr + + + + ) + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + { + + + + , +
+ + + + + + + } + + + + + + + + + { + + , + + } + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/html_set.xsl b/helm/style/style_prima_del_linguaggio_naturale/html_set.xsl new file mode 100644 index 000000000..6c7f66b1b --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/html_set.xsl @@ -0,0 +1,463 @@ + + + + + + + + + +http://localhost:8081/get?url= + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + Î + + + + + ) + + + ( + + + + + + Î + + + ) + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + Ï + + + + ) + + + ( + + Ï + + ) + + + + + + + + + + + + + + + Æ + + + + + + + + + + { + + : + + +
+ + + + | + + + + } + + + { + + : + + | + + } + + + + + + + { + + + + + , +
+ + + + + + + + } + + + { + + + + + } + + + , + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + Ç + + + + + ) + + + ( + + + + + + Ç + + + ) + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + È + + + + + ) + + + ( + + + + + + È + + + ) + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + Í + + + + + ) + + + ( + + + + + + Í + + + ) + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + Ì + + + + + ) + + + ( + + + + + + Ì + + + ) + + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + / + + + + + ) + + + ( + + + + + + / + + + ) + + + + + + + + + + + + | + + + + | + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/mml2mmlv1_0.xsl b/helm/style/style_prima_del_linguaggio_naturale/mml2mmlv1_0.xsl new file mode 100644 index 000000000..67e1accfb --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/mml2mmlv1_0.xsl @@ -0,0 +1,1957 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + 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/style_prima_del_linguaggio_naturale/mml2mmlv1_0_original.xsl b/helm/style/style_prima_del_linguaggio_naturale/mml2mmlv1_0_original.xsl new file mode 100644 index 000000000..44c34df74 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/mml2mmlv1_0_original.xsl @@ -0,0 +1,1848 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + + + + + 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/style_prima_del_linguaggio_naturale/mmlextension.xsl b/helm/style/style_prima_del_linguaggio_naturale/mmlextension.xsl new file mode 100644 index 000000000..39d2f5c47 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/mmlextension.xsl @@ -0,0 +1,1128 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 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_andrea.xsl b/helm/style/style_prima_del_linguaggio_naturale/mmlextension_andrea.xsl new file mode 100644 index 000000000..e75affee9 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/mmlextension_andrea.xsl @@ -0,0 +1,1052 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 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 new file mode 100644 index 000000000..dfe2e6aa3 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/mmlextension_irene.xsl @@ -0,0 +1,868 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 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 b/helm/style/style_prima_del_linguaggio_naturale/objcontent.xsl new file mode 100644 index 000000000..6ad0a4922 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/objcontent.xsl @@ -0,0 +1,232 @@ + + + + + + + + + + + + + + + + + + + + + type="text/xml" + href="" type="text/xsl" + type="xslt" + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +PROD + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + app + + + + + + + + + + + + + + + + + + + + + + + + + + $ + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/objcontent.xsl.csc b/helm/style/style_prima_del_linguaggio_naturale/objcontent.xsl.csc new file mode 100644 index 000000000..d2a846cba --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/objcontent.xsl.csc @@ -0,0 +1,223 @@ + + + + + + + + + + + + + + + + + + + + + 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 new file mode 100644 index 000000000..d3514b499 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/objcontent_old.xsl @@ -0,0 +1,220 @@ + + + + + + + + + + + + + + + + + + + + + type="text/xml" + href="" type="text/xsl" + type="xslt" + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +PROD + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + app + + + + + + + + + + + + + + + + + + + + + + + + + + $ + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/params.xsl b/helm/style/style_prima_del_linguaggio_naturale/params.xsl new file mode 100644 index 000000000..034eeba97 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/params.xsl @@ -0,0 +1,191 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 0 + + + + + + + + + + + + + + + + + + + + + + + + 0 + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/reals.xsl b/helm/style/style_prima_del_linguaggio_naturale/reals.xsl new file mode 100644 index 000000000..0e4afef94 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/reals.xsl @@ -0,0 +1,277 @@ + + + + + + + + + + + + + + +http://localhost:8081/get?url= + + + + + + + + + + + 0 + + + + 1 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 1 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + $x + + + + + + app + + $x + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + $x + + + app + + $x + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/ricerca.xsl b/helm/style/style_prima_del_linguaggio_naturale/ricerca.xsl new file mode 100644 index 000000000..e0fa13a93 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/ricerca.xsl @@ -0,0 +1,91 @@ + + + + + + + + + + + + +http://localhost:8081/get?url= + + + + + + + + + + + + + + + + + + + +
+ + + + + + + + + + + + + + + + +
+ + + + + + + + + + +
+ + + + + + + + +
+ + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/rootcontent.xsl b/helm/style/style_prima_del_linguaggio_naturale/rootcontent.xsl new file mode 100644 index 000000000..ada8b5cdd --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/rootcontent.xsl @@ -0,0 +1,29 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/rootcontent_withproofs.xsl b/helm/style/style_prima_del_linguaggio_naturale/rootcontent_withproofs.xsl new file mode 100644 index 000000000..11d668436 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/rootcontent_withproofs.xsl @@ -0,0 +1,29 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/roottheory.xsl b/helm/style/style_prima_del_linguaggio_naturale/roottheory.xsl new file mode 100644 index 000000000..d293ee6f2 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/roottheory.xsl @@ -0,0 +1,22 @@ + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/set.xsl b/helm/style/style_prima_del_linguaggio_naturale/set.xsl new file mode 100644 index 000000000..303c872ef --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/set.xsl @@ -0,0 +1,487 @@ + + + + + + + + + + + + + + +http://localhost:8081/get?url= + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/theory_content.xsl b/helm/style/style_prima_del_linguaggio_naturale/theory_content.xsl new file mode 100644 index 000000000..9b65cc5b2 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/theory_content.xsl @@ -0,0 +1,57 @@ + + + + + + + + + + + + + + + +http://localhost:8081/get?url= + + + + +
+ +
+ + + + + + +
+ +
+ + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/style_prima_del_linguaggio_naturale/theory_pres.xsl b/helm/style/style_prima_del_linguaggio_naturale/theory_pres.xsl new file mode 100644 index 000000000..9a96cdc03 --- /dev/null +++ b/helm/style/style_prima_del_linguaggio_naturale/theory_pres.xsl @@ -0,0 +1,34 @@ + + + + + + + + + + + + + + + + + + + BEGIN SECTION + + END SECTION + + + + + BEGIN SECTION + + END SECTION + + + + + -- 2.39.2