From: Claudio Sacerdoti Coen Date: Tue, 31 Oct 2000 17:17:10 +0000 (+0000) Subject: Initial revision X-Git-Tag: nogzip~221 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=aa87f28d3a96456e7cec9493c6533e5c146812e8;p=helm.git Initial revision --- diff --git a/helm/style/annotatedcont.xsl b/helm/style/annotatedcont.xsl new file mode 100644 index 000000000..e97d08f2b --- /dev/null +++ b/helm/style/annotatedcont.xsl @@ -0,0 +1,73 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/annotatedcont.xsl.csc b/helm/style/annotatedcont.xsl.csc new file mode 100644 index 000000000..3508d6be4 --- /dev/null +++ b/helm/style/annotatedcont.xsl.csc @@ -0,0 +1,66 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/annotatedpres.xsl b/helm/style/annotatedpres.xsl new file mode 100644 index 000000000..511f915f5 --- /dev/null +++ b/helm/style/annotatedpres.xsl @@ -0,0 +1,34 @@ + + + + + + + + + + + + + + + + +

+ + +

+ + + + + + + +

+ + + + diff --git a/helm/style/basic.xsl b/helm/style/basic.xsl new file mode 100644 index 000000000..93eb28052 --- /dev/null +++ b/helm/style/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/content.xsl b/helm/style/content.xsl new file mode 100644 index 000000000..24b97e6e6 --- /dev/null +++ b/helm/style/content.xsl @@ -0,0 +1,274 @@ + + + + + + + + + + + + + + + + + + + + + + +http://localhost:8081/get?url= + + + + + + + + + + + + + + + + + + + + + + arrow + + + + prod + + + + + + + + + + + + + + + + + cast + + + + + + + + + + + + + + + + + + + + + + + + + letin + + + + + let +

+ + + + + + + + + + + + + + + + app + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

+ + + + + + +

+ + + + + +

+ + mutcase + + +

+ + +

+ + + + + + + + + app + + + +

LAMBDA

+ + + +

LAMBDA

+ + + + + + +

+ fix +

+ + + + + + +

+ cofix +

+ + + + + + + + +

+ + + + + + +

+ + + + + diff --git a/helm/style/content.xsl.csc b/helm/style/content.xsl.csc new file mode 100644 index 000000000..5f7c1e131 --- /dev/null +++ b/helm/style/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/content_senza_tipi.13.9.00.xsl b/helm/style/content_senza_tipi.13.9.00.xsl new file mode 100644 index 000000000..7de998720 --- /dev/null +++ b/helm/style/content_senza_tipi.13.9.00.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/content_to_html.xsl b/helm/style/content_to_html.xsl new file mode 100644 index 000000000..dd1c07794 --- /dev/null +++ b/helm/style/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/html_init.xsl b/helm/style/html_init.xsl new file mode 100644 index 000000000..9e81b169c --- /dev/null +++ b/helm/style/html_init.xsl @@ -0,0 +1,259 @@ + + + + + + + + + +http://localhost:8081/get?url= + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + + + + + + + + ) + + + ( + + + + + + + + + + + ) + + + + + + + + + + + + + + + + + + + - + + + + + + + + + + + + ( + + + +
+ + + + + + + + - + + + + + ) + + + ( + + + + + + - + + + ) + + + + + + + + + + + + + + + + + + + Ø + + + + + + + + + + + + + + + + + + + + + + $ + + + : + + + +
+ + + + . + + + + + + + + + + $ + + + : + + . + + + + + + + + + + + + + + + + +

+ + + + + + + + + + + + + + + + + + diff --git a/helm/style/html_reals.xsl b/helm/style/html_reals.xsl new file mode 100644 index 000000000..04ff478c5 --- /dev/null +++ b/helm/style/html_reals.xsl @@ -0,0 +1,234 @@ + + + + + + + + + +http://localhost:8081/get?url= + + + + + + + + + + + + + + + + + + + lim + + _{+
+ ®
+
+} +
+ + + + + + + + + + + + + lim + + _{+
+ ®
+
+} + + + + + + + + + + + + + + + + + + + + ^d + / + _{+ d
+
+} + + + + + + + + + + + + + + | + + + + | + + + + + + + + + + + + + + ! + + + + + + + + + + + (sqr + + + + ) + + + + + + + + + + + + ^{+
+} + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + { + + + + , +
+ + + + + + + } + + + + + + + + + { + + , + + } + + + + + + + + + + +

+ + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/html_set.xsl b/helm/style/html_set.xsl new file mode 100644 index 000000000..6c7f66b1b --- /dev/null +++ b/helm/style/html_set.xsl @@ -0,0 +1,463 @@ + + + + + + + + + +http://localhost:8081/get?url= + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + Î + + + + + ) + + + ( + + + + + + Î + + + ) + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + Ï + + + + ) + + + ( + + Ï + + ) + + + + + + + + + + + + + + + Æ + + + + + + + + + + { + + : + + +
+ + + + | + + + + } + + + { + + : + + | + + } + + + + + + + { + + + + + , +
+ + + + + + + + } + + + { + + + + + } + + + , + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + Ç + + + + + ) + + + ( + + + + + + Ç + + + ) + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + È + + + + + ) + + + ( + + + + + + È + + + ) + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + Í + + + + + ) + + + ( + + + + + + Í + + + ) + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + Ì + + + + + ) + + + ( + + + + + + Ì + + + ) + + + + + + + + + + + + + + + + + + + ( + + + +
+ + + + + + + + / + + + + + ) + + + ( + + + + + + / + + + ) + + + + + + + + + + + + | + + + + | + + + + + + + + +

+ + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/mml2mmlv1_0.xsl b/helm/style/mml2mmlv1_0.xsl new file mode 100644 index 000000000..67e1accfb --- /dev/null +++ b/helm/style/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

+ + + + + + + + + + + + + + + + + +

+ + +

+ +

+ + +

+ + + +

+ + +

+ + + + + + +

+ + +

+ + + + + + + + + + + + + + + + +

+ + + + +

+ + + + + + + + + + + + + + + +

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/mml2mmlv1_0_original.xsl b/helm/style/mml2mmlv1_0_original.xsl new file mode 100644 index 000000000..44c34df74 --- /dev/null +++ b/helm/style/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/mmlextension.xsl b/helm/style/mmlextension.xsl new file mode 100644 index 000000000..566ccdf0a --- /dev/null +++ b/helm/style/mmlextension.xsl @@ -0,0 +1,1382 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 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 + + + + + + + + + + __ + + + | + _ + + +

+ _ + + + + + + + + + + + + + + + + + + + VARIABLE OF TYPE + + + + + + + __ + + + + + + + + + + + + + + + + + + + + + + + + + : + + + + + + + + + + + + : + + + + + + + + + + + + + + +

+ + +

+ + + + + + + + + Π + + + + + + + . + + + + + + + + Π + + : + + . + + + + + + + + + + + + ( + + + + + + + + → + + + + + + + + ) + + + + + + + ( + + → + + ) + + + + + + + + + + + ( + + + + + + + + + ( + + + + + + + + + ) + + + + + + + ( + + + _ + + + ) + + + + + + + + + + + ( + + + + + + + + :> + + + + + + + + ) + + + + + + + ( + + :> + + ) + + + + + Prop + + + Set + + + Type + + + + +

+ + + + + < + + + > + CASES + _ + + + + + + + + + + > + CASES + _ + + + + + + + + + OF + + + + +

+ + + + + + | + + + | + + + _ + + + ⇒ + + + + + + + + + + |_ + ⇒ + + + + + + + + + + END + + + + + + + <

> + CASES + _ + + _ + OF + + + + | + + + + ⇒ + + + _ + END +

+ + + + + + + + + + FIX + _ +

+ { + + + + + + + __ + + +

+ + + +

+ : + + + + + + + + + + + := + + + + + + + + + := + + + + + + + + + + + + + } + + + + + + + FIX +

+ { + + + + + +

+ : + + := + + + } + + + + + + + + + + + + + + + + + COFIX + _ +

+ { + + + + + + + __ + + +

+ + + +

+ : + + + + + + + + + + + := + + + + + + + + + := + + + + + + + + + + + + + } + + + + + + + COFIX +

+ { + + + + + +

+ : + + := + + + } + + + + + + + + + + + + + + + + + + + + + + + + + we proved + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + ) + + + + + + + + + + + + + Consider + + + + + + + + + + + + + + + Rewrite + _ + + _ + with + _ + + _ + by + _ + + _ + in + _ + + _ + and apply + _ + + + + + + + + + + + + + + + + + Consider + + + + + + + + + In particular, we have + + + + + + ( + + ) + + + + + + + + ( + + ) + + + + + + + + + + + + + + + + + + + + + + + + Consider + _ + + + + + + + + + We prove + _ + + _ + by cases: + + + + + + * + + + + + + + + * + + + + + + + + ERROR + + + + + + +

+ + + + + + Rewrite + _ + + _ + with + _ + + _ + by + _ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

+ + + + + + + λ + + + + + + + . + + + + + + + + λ + + : + + . + + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + + + + + + __ + + = + + + + + + + + ) + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + + + + + + __ + + + + + + + + + + ) + + + + + + + + + + + + + + + + + + + + + + + + + + + + + { + + + + + + { + | + + + + + + } + + + + + + + + + { + + + , + + + + + + + { + + + , + + + + + + + } + + + + + + + + + + + + + + + + | + + | + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

+ + + + + + + + + + + + + + + + + + + + + + + +

+ + +

+ + + + + + + + > + + + + + + + + + + + diff --git a/helm/style/mmlextension_andrea.xsl b/helm/style/mmlextension_andrea.xsl new file mode 100644 index 000000000..b4bbcdbdb --- /dev/null +++ b/helm/style/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 + + + + + + + + + + __ + + + | + _ + + +

+ _ + + + + + + + + + + + + + + + + + + + VARIABLE OF 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 new file mode 100644 index 000000000..90852b79e --- /dev/null +++ b/helm/style/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 + + + + + + + + + + __ + + + | + _ + + +

+ _ + + + + + + + + + + + + + + + + + + + VARIABLE OF TYPE + + + + + + + __ + + + + + + + + + + + + + + + +

+ + + + + +

+ + + + + Π + + : + + + + + + + + + + + . + + + + + + + + + . + + + + + + + + Π + + : + + . + + + + + + + + + + + + ( + + + + + + + + → + + + + + + + + ) + + + + + + + ( + + → + + ) + + + + + + + + + + + ( + + + + + + + + + ( + + + + + + + + + ) + + + + + + + ( + + + _ + + + ) + + + + + + + + + + + ( + + + + + + + + :> + + + + + + + + ) + + + + + + + ( + + :> + + ) + + + + + Prop + + + Set + + + Type + + + + +

+ + + + + < + + + > + CASES + _ + + + + + + + + + + > + CASES + _ + + + + + + + + + OF + + + + +

+ + + + + + | + + + | + + + _ + + + ⇒ + + + + + + + + + + |_ + ⇒ + + + + + + + + + + END + + + + + + + <

> + CASES + _ + + _ + OF + + + + | + + + + ⇒ + + + _ + END +

+ + + + + + + + + + FIX + _ +

+ { + + + + + + + __ + + +

+ + + +

+ : + + + + + + + + + + + := + + + + + + + + + := + + + + + + + + + + + + + } + + + + + + + FIX +

+ { + + + + + +

+ : + + := + + + } + + + + + + + + + + + + + + + + + COFIX + _ +

+ { + + + + + + + __ + + +

+ + + +

+ : + + + + + + + + + + + := + + + + + + + + + := + + + + + + + + + + + + + } + + + + + + + COFIX +

+ { + + + + + +

+ : + + := + + + } + + + + + + + + + + + + + + + + +

+ + + +

+ + + + + λ + + + : + + + + + + + + + + + . + + + + + + + + + . + + + + + + + + λ + + : + + . + + + + + + + + + + + + + + + +

+ + + + + + + + + + + + + + + + + + +

+ + +

+ + + + + + + + > + + + + + + + + diff --git a/helm/style/objcontent.xsl b/helm/style/objcontent.xsl new file mode 100644 index 000000000..6ad0a4922 --- /dev/null +++ b/helm/style/objcontent.xsl @@ -0,0 +1,232 @@ + + + + + + + + + + + + + + + + + + +

+ type="text/xml" + href="" type="text/xsl" + type="xslt" + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +PROD + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + app + +

+ + + + + +

+ + + + + + + + + + + + + + + + + + $ +

+ + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/objcontent.xsl.csc b/helm/style/objcontent.xsl.csc new file mode 100644 index 000000000..d2a846cba --- /dev/null +++ b/helm/style/objcontent.xsl.csc @@ -0,0 +1,223 @@ + + + + + + + + + + + + + + + + + + +

+ 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 new file mode 100644 index 000000000..d3514b499 --- /dev/null +++ b/helm/style/objcontent_old.xsl @@ -0,0 +1,220 @@ + + + + + + + + + + + + + + + + + + +

+ type="text/xml" + href="" type="text/xsl" + type="xslt" + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +PROD + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + app + +

+ + + + + +

+ + + + + + + + + + + + + + + + + + $ +

+ + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/params.xsl b/helm/style/params.xsl new file mode 100644 index 000000000..034eeba97 --- /dev/null +++ b/helm/style/params.xsl @@ -0,0 +1,191 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 0 + + + + + + + + + + + + + + + + + + + + + + + + 0 + + + + + + + + + + + diff --git a/helm/style/proof31-10-00.xsl b/helm/style/proof31-10-00.xsl new file mode 100644 index 000000000..3c4234307 --- /dev/null +++ b/helm/style/proof31-10-00.xsl @@ -0,0 +1,210 @@ + + + + + + + + + + + + + + +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/proofs.xsl b/helm/style/proofs.xsl new file mode 100644 index 000000000..88af829f8 --- /dev/null +++ b/helm/style/proofs.xsl @@ -0,0 +1,243 @@ + + + + + + + + + + + + + + +http://localhost:8081/get?url= + + + + + + + + + + + + + + + + + + thread + + + rw_step + + + + + + + + + + thread + + + app + + + + + + + + + and_ind + +

+ +

+ + + + + + + or_ind + + + + + + + + + proof + + + + + + + + + + + + + + + + + + + + + + prev + + + + + + + + + + + + + + + rw_step + + + + + + + + + thread + + + + + + + + + + + + + + + + + + + + + + + + + + + rewrite_and_apply + + rw_step + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + app + + + + + + + + + + + app + + * + * + * + + + + + + app + + + + + + + + + + + + + + diff --git a/helm/style/reals.xsl b/helm/style/reals.xsl new file mode 100644 index 000000000..6c47f9562 --- /dev/null +++ b/helm/style/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/ricerca.xsl b/helm/style/ricerca.xsl new file mode 100644 index 000000000..e0fa13a93 --- /dev/null +++ b/helm/style/ricerca.xsl @@ -0,0 +1,91 @@ + + + + + + + + + + + + +http://localhost:8081/get?url= + + + + + + + + + + + + + + + + + + + +
+ + + + + + + + + + + + + + + + +
+ + + + + + + + + + +
+ + + + + + + + +
+ + + + + + + + + + + + + diff --git a/helm/style/rootcontent.xsl b/helm/style/rootcontent.xsl new file mode 100644 index 000000000..9e85f0344 --- /dev/null +++ b/helm/style/rootcontent.xsl @@ -0,0 +1,30 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/rootcontent_withproofs.xsl b/helm/style/rootcontent_withproofs.xsl new file mode 100644 index 000000000..11d668436 --- /dev/null +++ b/helm/style/rootcontent_withproofs.xsl @@ -0,0 +1,29 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/roottheory.xsl b/helm/style/roottheory.xsl new file mode 100644 index 000000000..d293ee6f2 --- /dev/null +++ b/helm/style/roottheory.xsl @@ -0,0 +1,22 @@ + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/set.xsl b/helm/style/set.xsl new file mode 100644 index 000000000..303c872ef --- /dev/null +++ b/helm/style/set.xsl @@ -0,0 +1,487 @@ + + + + + + + + + + + + + + +http://localhost:8081/get?url= + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/theory_content.xsl b/helm/style/theory_content.xsl new file mode 100644 index 000000000..9b65cc5b2 --- /dev/null +++ b/helm/style/theory_content.xsl @@ -0,0 +1,57 @@ + + + + + + + + + + + + + + + +http://localhost:8081/get?url= + + + + +

+ + + + + + +

+ + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/theory_pres.xsl b/helm/style/theory_pres.xsl new file mode 100644 index 000000000..9a96cdc03 --- /dev/null +++ b/helm/style/theory_pres.xsl @@ -0,0 +1,34 @@ + + + + + + + + + + + + + + + + + + + BEGIN SECTION +

+ END SECTION + + + + + BEGIN SECTION +

+ END SECTION + + + + +