X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fstyle_prima_del_linguaggio_naturale%2Fmmlextension_andrea.xsl;fp=helm%2Fstyle%2Fstyle_prima_del_linguaggio_naturale%2Fmmlextension_andrea.xsl;h=e75affee97ca6b64a2d358e8cd2ba6ede661c273;hb=aabc65e7ce88b0a625e83449f1f8fceda3be393a;hp=0000000000000000000000000000000000000000;hpb=aa87f28d3a96456e7cec9493c6533e5c146812e8;p=helm.git 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 + + { + + + + + + + : + + := + + + } + + + + + + + + + + + + + + + + + + + + + + + + λ + + + + + + + . + + + + + + + + λ + + : + + . + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + + + + + + + __ + + + + + + + + + + + ) + + + + + + + + + + + + + + + + + + + + + + { + + + + + + __ + | + + + + + + } + + + + + + + + + { + + + , + + + + + + + _ + + + , + + + + + + + } + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + > + + + + + + + +