From 124f4cc530827721444de874e1a04ee5012586b1 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 19 Jan 2004 15:25:01 +0000 Subject: [PATCH] No longer in use. The official repository for the stylesheet is now the repository of mowgli. --- helm/meta_style/.cvsignore | 6 - helm/meta_style/Makefile | 65 - helm/meta_style/algebra.xml | 205 -- helm/meta_style/arith.xml | 67 - helm/meta_style/basic.xml | 88 - helm/meta_style/list.xml | 60 - helm/meta_style/meta_cic2mathml.xsl | 1287 --------- helm/meta_style/modeset.xsl | 65 - helm/meta_style/operator.dtd | 71 - helm/meta_style/positive.xsl | 218 -- helm/meta_style/reals.xml | 163 -- helm/meta_style/set.xml | 333 --- helm/meta_style/subst.pl | 17 - helm/meta_style/xslt_index.txt | 8 - helm/style/annotatedcont.xsl | 122 - helm/style/annotatedpres.xsl | 58 - helm/style/content.xsl | 377 --- helm/style/content_to_html.xsl | 2436 ---------------- helm/style/contentlib.xsl | 116 - helm/style/diseq.xsl | 336 --- helm/style/drop_coercions.xsl | 184 -- helm/style/expandobj.xsl | 85 - helm/style/genmmlid.xsl | 55 - helm/style/getter.xsl | 34 - helm/style/headercontent.xsl | 47 - helm/style/html_init.xsl | 507 ---- helm/style/html_reals.xsl | 469 --- helm/style/html_set.xsl | 389 --- helm/style/inductive.xsl | 416 --- helm/style/ite.xsl | 48 - helm/style/lambda.xsl | 158 - helm/style/link.xsl | 127 - helm/style/links_library.xsl | 363 --- helm/style/logic.xsl | 155 - helm/style/mk_dep_graph.xsl | 38 - helm/style/mk_meta_and_dep_graph.xsl | 265 -- helm/style/mk_meta_graph.xsl | 38 - helm/style/mk_meta_theory.xsl | 171 -- helm/style/mmlctop.xsl | 4005 -------------------------- helm/style/mmlctop.xsl-0.14 | 3103 -------------------- helm/style/mmlctop2_0.xsl | 3985 ------------------------- helm/style/mmlextension.xsl | 2382 --------------- helm/style/mmlnotation.xsl | 397 --- helm/style/mmltheoryextension.xsl | 42 - helm/style/objcontent.xsl | 242 -- helm/style/objtheorycontent.xsl | 85 - helm/style/params.xsl | 430 --- helm/style/proofs.xsl | 559 ---- helm/style/rewrite.xsl | 135 - helm/style/ricerca.xsl | 104 - helm/style/ring.xsl | 134 - helm/style/rootcontent.xsl | 94 - helm/style/roottheory.xsl | 44 - helm/style/show_dc.xsl | 249 -- helm/style/theory_content.xsl | 90 - helm/style/theory_pres.xsl | 127 - helm/style/xslt_index.txt | 40 - 57 files changed, 25894 deletions(-) delete mode 100644 helm/meta_style/.cvsignore delete mode 100644 helm/meta_style/Makefile delete mode 100644 helm/meta_style/algebra.xml delete mode 100644 helm/meta_style/arith.xml delete mode 100644 helm/meta_style/basic.xml delete mode 100644 helm/meta_style/list.xml delete mode 100644 helm/meta_style/meta_cic2mathml.xsl delete mode 100644 helm/meta_style/modeset.xsl delete mode 100644 helm/meta_style/operator.dtd delete mode 100644 helm/meta_style/positive.xsl delete mode 100644 helm/meta_style/reals.xml delete mode 100644 helm/meta_style/set.xml delete mode 100755 helm/meta_style/subst.pl delete mode 100644 helm/meta_style/xslt_index.txt delete mode 100644 helm/style/annotatedcont.xsl delete mode 100644 helm/style/annotatedpres.xsl delete mode 100644 helm/style/content.xsl delete mode 100644 helm/style/content_to_html.xsl delete mode 100644 helm/style/contentlib.xsl delete mode 100644 helm/style/diseq.xsl delete mode 100644 helm/style/drop_coercions.xsl delete mode 100644 helm/style/expandobj.xsl delete mode 100644 helm/style/genmmlid.xsl delete mode 100644 helm/style/getter.xsl delete mode 100644 helm/style/headercontent.xsl delete mode 100644 helm/style/html_init.xsl delete mode 100644 helm/style/html_reals.xsl delete mode 100644 helm/style/html_set.xsl delete mode 100644 helm/style/inductive.xsl delete mode 100644 helm/style/ite.xsl delete mode 100644 helm/style/lambda.xsl delete mode 100644 helm/style/link.xsl delete mode 100644 helm/style/links_library.xsl delete mode 100644 helm/style/logic.xsl delete mode 100644 helm/style/mk_dep_graph.xsl delete mode 100644 helm/style/mk_meta_and_dep_graph.xsl delete mode 100644 helm/style/mk_meta_graph.xsl delete mode 100644 helm/style/mk_meta_theory.xsl delete mode 100644 helm/style/mmlctop.xsl delete mode 100755 helm/style/mmlctop.xsl-0.14 delete mode 100644 helm/style/mmlctop2_0.xsl delete mode 100644 helm/style/mmlextension.xsl delete mode 100644 helm/style/mmlnotation.xsl delete mode 100644 helm/style/mmltheoryextension.xsl delete mode 100644 helm/style/objcontent.xsl delete mode 100644 helm/style/objtheorycontent.xsl delete mode 100644 helm/style/params.xsl delete mode 100644 helm/style/proofs.xsl delete mode 100644 helm/style/rewrite.xsl delete mode 100644 helm/style/ricerca.xsl delete mode 100644 helm/style/ring.xsl delete mode 100644 helm/style/rootcontent.xsl delete mode 100644 helm/style/roottheory.xsl delete mode 100644 helm/style/show_dc.xsl delete mode 100644 helm/style/theory_content.xsl delete mode 100644 helm/style/theory_pres.xsl delete mode 100644 helm/style/xslt_index.txt diff --git a/helm/meta_style/.cvsignore b/helm/meta_style/.cvsignore deleted file mode 100644 index b20cfb281..000000000 --- a/helm/meta_style/.cvsignore +++ /dev/null @@ -1,6 +0,0 @@ -algebra.xsl -arith.xsl -basic.xsl -reals.xsl -set.xsl -list.xsl diff --git a/helm/meta_style/Makefile b/helm/meta_style/Makefile deleted file mode 100644 index f51cc8094..000000000 --- a/helm/meta_style/Makefile +++ /dev/null @@ -1,65 +0,0 @@ -XSLTPROC = xsltproc --timing -FORMAT = xmllint --format -SUBST = ./subst.pl -METASTYLESHEET = ./meta_cic2mathml.xsl -TMP1 = .tmpfile1 -TMP2 = .tmpfile2 - -all: algebra.xsl arith.xsl basic.xsl reals.xsl set.xsl list.xsl - -clean: - rm -f algebra.xsl arith.xsl basic.xsl reals.xsl set.xsl list.xsl - -algebra.xsl: algebra.xml $(METASTYLESHEET) - @echo "**** PROCESSING algebra.xml ****" - @$(XSLTPROC) $(METASTYLESHEET) algebra.xml > $(TMP1) - @$(FORMAT) $(TMP1) > $(TMP2) - @mv $(TMP2) algebra.xsl - @rm $(TMP1) - @$(SUBST) oxsl: xsl: algebra.xsl - @$(SUBST) xmlns:oxsl xmlns:xsl algebra.xsl - -arith.xsl: arith.xml $(METASTYLESHEET) - @echo "**** PROCESSING arith.xml ****" - @$(XSLTPROC) $(METASTYLESHEET) arith.xml > $(TMP1) - @$(FORMAT) $(TMP1) > $(TMP2) - @mv $(TMP2) arith.xsl - @rm $(TMP1) - @$(SUBST) oxsl: xsl: arith.xsl - @$(SUBST) xmlns:oxsl xmlns:xsl arith.xsl - -basic.xsl: basic.xml $(METASTYLESHEET) - @echo "**** PROCESSING basic.xml ****" - @$(XSLTPROC) $(METASTYLESHEET) basic.xml > $(TMP1) - @$(FORMAT) $(TMP1) > $(TMP2) - @mv $(TMP2) basic.xsl - @rm $(TMP1) - @$(SUBST) oxsl: xsl: basic.xsl - @$(SUBST) xmlns:oxsl xmlns:xsl basic.xsl - -reals.xsl: reals.xml $(METASTYLESHEET) - @echo "**** PROCESSING reals.xml ****" - @$(XSLTPROC) $(METASTYLESHEET) reals.xml > $(TMP1) - @$(FORMAT) $(TMP1) > $(TMP2) - @mv $(TMP2) reals.xsl - @rm $(TMP1) - @$(SUBST) oxsl: xsl: reals.xsl - @$(SUBST) xmlns:oxsl xmlns:xsl reals.xsl - -set.xsl: set.xml $(METASTYLESHEET) - @echo "**** PROCESSING set.xml ****" - @$(XSLTPROC) $(METASTYLESHEET) set.xml > $(TMP1) - @$(FORMAT) $(TMP1) > $(TMP2) - @mv $(TMP2) set.xsl - @rm $(TMP1) - @$(SUBST) oxsl: xsl: set.xsl - @$(SUBST) xmlns:oxsl xmlns:xsl set.xsl - -list.xsl: list.xml $(METASTYLESHEET) - @echo "**** PROCESSING list.xml ****" - @$(XSLTPROC) $(METASTYLESHEET) list.xml > $(TMP1) - @$(FORMAT) $(TMP1) > $(TMP2) - @mv $(TMP2) list.xsl - @rm $(TMP1) - @$(SUBST) oxsl: xsl: list.xsl - @$(SUBST) xmlns:oxsl xmlns:xsl list.xsl diff --git a/helm/meta_style/algebra.xml b/helm/meta_style/algebra.xml deleted file mode 100644 index 696a19a1b..000000000 --- a/helm/meta_style/algebra.xml +++ /dev/null @@ -1,205 +0,0 @@ - - - - - - - - 0 - - - - 1 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - app - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/meta_style/arith.xml b/helm/meta_style/arith.xml deleted file mode 100644 index a21a51306..000000000 --- a/helm/meta_style/arith.xml +++ /dev/null @@ -1,67 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/meta_style/basic.xml b/helm/meta_style/basic.xml deleted file mode 100644 index e9da62a62..000000000 --- a/helm/meta_style/basic.xml +++ /dev/null @@ -1,88 +0,0 @@ - - - - - - - - - - - - - - iff - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/meta_style/list.xml b/helm/meta_style/list.xml deleted file mode 100644 index 9ed07d69b..000000000 --- a/helm/meta_style/list.xml +++ /dev/null @@ -1,60 +0,0 @@ - - - - - - - - - - - append - - - - - - - - - - - - - - diff --git a/helm/meta_style/meta_cic2mathml.xsl b/helm/meta_style/meta_cic2mathml.xsl deleted file mode 100644 index 072774b5d..000000000 --- a/helm/meta_style/meta_cic2mathml.xsl +++ /dev/null @@ -1,1287 +0,0 @@ - - - - - - - - - - Copyright (C) 2000, HELM Team - - This file is part of HELM, an Hypertextual, Electronic - Library of Mathematics, developed at the Computer Science - Department, University of Bologna, Italy. - - HELM is free software; you can redistribute it and/or - modify it under the terms of the GNU General Public License - as published by the Free Software Foundation; either version 2 - of the License, or (at your option) any later version. - - HELM is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License - along with HELM; if not, write to the Free Software - Foundation, Inc., 59 Temple Place - Suite 330, Boston, - MA 02111-1307, USA. - - For details, see the HELM World-Wide-Web page, - http://cs.unibo.it/helm/. - - - - - - - - - - - - - - - - - - - - - - - - - false - true - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - false - true - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - and count(*) = 2 - - - - - - - *[2]/ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - instantiate/ - - - - - CONST[@uri='cic:/Coq/Init/Logic/not.con'] and - - - - - - - - - - APPLY[ - - ] - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - {@id} - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - {@id} - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - app - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - /decl/@binder - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - CONST - MUTIND - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *[2]/ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - instantiate/ - - - - APPLY/ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - helm:xref - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - {@id} - - - - - @id - @uri - - - - - - - - - - - - - - - - - - diff --git a/helm/meta_style/modeset.xsl b/helm/meta_style/modeset.xsl deleted file mode 100644 index 9c0af40ea..000000000 --- a/helm/meta_style/modeset.xsl +++ /dev/null @@ -1,65 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/meta_style/operator.dtd b/helm/meta_style/operator.dtd deleted file mode 100644 index c76466956..000000000 --- a/helm/meta_style/operator.dtd +++ /dev/null @@ -1,71 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/meta_style/positive.xsl b/helm/meta_style/positive.xsl deleted file mode 100644 index e337b663e..000000000 --- a/helm/meta_style/positive.xsl +++ /dev/null @@ -1,218 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 0 - - - - - - - - - - - - - - 1 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/meta_style/reals.xml b/helm/meta_style/reals.xml deleted file mode 100644 index b4cdf2d8a..000000000 --- a/helm/meta_style/reals.xml +++ /dev/null @@ -1,163 +0,0 @@ - - - - - - - - 0 - - - - 1 - - - - - - - - - - - - - 2 - - - - - - - - - - 1 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/meta_style/set.xml b/helm/meta_style/set.xml deleted file mode 100644 index 0dbcd3761..000000000 --- a/helm/meta_style/set.xml +++ /dev/null @@ -1,333 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/meta_style/subst.pl b/helm/meta_style/subst.pl deleted file mode 100755 index 27ca245d5..000000000 --- a/helm/meta_style/subst.pl +++ /dev/null @@ -1,17 +0,0 @@ -#!/usr/bin/perl - - -open(FILE, $ARGV[2]) || die("Error: cannot open \"$ARGV[2]\" for reading.\n"); -@file = ; -close(FILE); - -open(FILE, ">$ARGV[2]"); - -foreach $line (@file) -{ - $line =~ s/$ARGV[0]/$ARGV[1]/g; - - print FILE "$line"; -} - -close(FILE); diff --git a/helm/meta_style/xslt_index.txt b/helm/meta_style/xslt_index.txt deleted file mode 100644 index 2f683f28d..000000000 --- a/helm/meta_style/xslt_index.txt +++ /dev/null @@ -1,8 +0,0 @@ -algebra.xsl -arith.xsl -basic.xsl -reals.xsl -set.xsl -list.xsl -positive.xsl -modeset.xsl diff --git a/helm/style/annotatedcont.xsl b/helm/style/annotatedcont.xsl deleted file mode 100644 index 9cc298f09..000000000 --- a/helm/style/annotatedcont.xsl +++ /dev/null @@ -1,122 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/annotatedpres.xsl b/helm/style/annotatedpres.xsl deleted file mode 100644 index 61d6211a8..000000000 --- a/helm/style/annotatedpres.xsl +++ /dev/null @@ -1,58 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/content.xsl b/helm/style/content.xsl deleted file mode 100644 index 001ff876d..000000000 --- a/helm/style/content.xsl +++ /dev/null @@ -1,377 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - let_in - - - - - - - - - - - - - - - - - - - - - - - - - - arrow - - - - - - forall - - - prod - - - - - - - - - - - - - - - - - - - - - - - - - cast - - - - - - - - - - - - - - - - - - - - - - - - app - - - - - - - - - - - - - - - - - - - meta - - - - ? - - - - - - - - - - - _ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - mutcase - - - - - - - - - LAMBDA - - - - - - - - - app - - - - LAMBDA - - - - - - - - - - - - - - fix - - - - - - - - - - cofix - - - - - - - - - - - - - inst - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl deleted file mode 100644 index 56231b2bc..000000000 --- a/helm/style/content_to_html.xsl +++ /dev/null @@ -1,2436 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ??? - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ??? - - - - - - - - - - - - - - - - - <xsl:value-of select="$CICURI"/> - - - - - - if(document.getElementById) - for(var i=0;i<document.to_be_deleted.length;i++) - Hide(document.getElementById(document.to_be_deleted[i])); - - - - - - - - - - - - - - - - - - - - - - - - - -   - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - : - - . - - - - - - - - - - : - - . - - - - - ( - - - - - - - - ) - - - - ( - - - - - - - - ) - - - - ( - - - - - - - - ) - - - - ( - - -   - - - ) - - - - ( - - : - - ) - - - Prop - - - Set - - - Type - - - - < - - > - CASE - - OF - - - - - | - - - - - - - - - - - - - - - { - - - / - - - - - - - - } - - - - - FIX - - { - - - : - - := - - - - } - - - ; - - - - - - - COFIX - - { - - - : - - := - - - - } - - - ; - - - - - - - if - - then - - else - - - - - -  proves  - - -  which is equivalent to  - - - - - - letin1 (inline error) - - - - - Contradiction. - - - - From  - -  we get - ( - - )  - -  and  - ( - - )  - - ; -  hence  - - - - - - [ - - - - - - - - - - - - - - - - - - - - - ] - - - - - - - - - - - - - - - - - - - - - - - - - - - - ( - - ) - - - - - - - - - - - - - - - - - - - - - - - - - ( - - ) - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - * - - - - - - - - - - - - - - - - * - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - * - - - - - - - - - - - - - - - - * - - - - - - - - - - - | - - - | - - - - - - | - - - | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - [ - - ] - - - - - - - - - - - - - : - - . - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - : - - - -
- - - - . - - - -
- - - -
-
- - - - - - - - - - - : - - -
- - - - . - - - -
- - - -
-
- - - - - ( - - - -
- - - - - - - - - - - - - ) -
- - - -
-
- - - - - ( - - - -
- - - - - - - - - - - - - ) -
- - - -
-
- - - - - ( - - - -
- - - - - - - - - - - - - ) -
- - - -
-
- - - - - ( - - - - -
- - - - - - -
- ) -
- - - -
-
- - - - - - ( - - -
- - - :> - - - - ) -
- - - -
-
- - - - - -
-
- - Prop - - - Set - - - Type - - - - - < - - - - > -
- - - CASE - - - - OF - - -
- - - - - -    - - - | - - - - - - - - - - - - - -
- - - - - - -
- - - -
-
-
- - - -
-
- - - - - FIX - - { - -
- - - - - : - - - -
- - - - := - - - -
-
- - - - } -
- - - -
-
- - - - - COFIX - - { -
- - - - - - : - - - -
- - - - := - - - - -
-
- - - - } -
- - - -
-
- - let  - -  :=  - - - -
- - - - in  - - - -
- - - if - - - -
- - - - then - - - -
- - - - else - - - -
- - - - - - - - - - - - - - -   - -
- - - - we proved  - - - -
- - - - and by delta equivalence - - - -
-
- - -
- - - - we proved  -
- - - -
- - - -
- - - - - - - - - - - -   - - - - - - - - - - - We have the following equality chain: - - -
- - - - - - - - -  = - - - - - - - - - -
- - - - - - -
-
-
- - - We have the following chain of disequalities: - - -
- - - - - - - - -   - - - - -   - - - - - - -
- - - - - - -
-
-
- - - - - -
- - - - - - -
- - - - - - -
- - - -
- - - -
- - - ( - - ) - - - - - - - - - - - - - - Consider  - - - - - - - - - - - - - - - - - - -
- - - - Rewrite  - -   - -
- - - -
- with  - -   - -
- - - -
- by  - - - -
- - - - - -
- - - - Then apply it to  - -
- - - We prove  - - - -
- - - - by induction on  - - - - - - - - -
- - -
- - - - Case  - - - - -
- - - - By induction hypothesis, we have: - -
- - - - ( - - - - - -
-
-
- - - - - - - -
- - - - - - - - ( - - -   - - : - - - ) - - - - - - - - -
- - - - Contradiction. -
- - - - - - - - - - Consider  - - - -
- - - - In particular, we have -
- - - - ( - - )  - - - -
- - - - ( - - )  - - - -
- - - - - - -
- - - - - - - - - - Consider  - - - -
- - - - We proceed by cases to prove  - -
- - - - Left: suppose  - ( - - - -
- - - - - - -
- - - - Right: suppose  - ( - - - -
- - - - - - -
- - - - - - - - - - Consider  - - - -
- - - - We prove  - -  by cases: -
- - - - Left:  - - - -
- - - - Right:  - - - -
- - - - - - - - - - Consider  - - - - - -
- - - - Let  - - : - -  such that -
- - - - ( - - ) - - - -
- - - - - - -
- - - - - - [ - - - - - - - - - - - - - - - - - - - - - ] - - - - - - - - - - - - - - - - - - - - - - - - - - - - ( - - ) - - - - - - - - - - - - - - - - - - - - - - - - - ( - - ) - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - * - - - - - - - - - - - - - - - - * - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - * - - - - - - - - - - - - - - - - * - - - - - - - - - - - | - - - | - - - - - - | - - - | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - [ - - ] - - -
-
- - - - - - - - - - - - - - - - - - - - - : - - -
- - - - . - - - -
- - - -
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

-DEFINITION ()
-TYPE =
- - - - - -
-BODY =
- - - - - - -

-
- - - - - -

-AXIOM ()
-TYPE =
- - - - - - -

-
- - - - - -

-UNFINISHED PROOF ()
-THESIS: - -
-CONJECTURES: - -
- - - - - - - - - - - - _ - - - : - - - - - - - - - - - _ - - - := - - - - - - _ :? _ - - - - |- : - - - -
-
-PROOF: - - - -

-
- - - - - -

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

-
- - - - - -

-VARIABLE
-TYPE = - - - -
-BODY = - - -
-

-
- - - - - - - - - -

BEGIN OF SECTION

- -

END OF SECTION

-
- -
diff --git a/helm/style/contentlib.xsl b/helm/style/contentlib.xsl deleted file mode 100644 index 00671bd5e..000000000 --- a/helm/style/contentlib.xsl +++ /dev/null @@ -1,116 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - interp - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/diseq.xsl b/helm/style/diseq.xsl deleted file mode 100644 index dd3650db7..000000000 --- a/helm/style/diseq.xsl +++ /dev/null @@ -1,336 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diseq_chain - - - - - - - - - - - - - - - - diseq_chain - - - - - - - - - - - - - - - - diseq_chain - - - - - - - - - - - - - - - - diseq_chain - - - - - - - - - - - - - - - - diseq_chain - - - - - - - - - - - - - - - - diseq_chain - - - - - - - - - - - - - - - - diseq_chain - - - - - - - - - - - - - - - - diseq_chain - - - - - - - - - - - - - - - - diseq_chain - - - - - - - - - - - - - - - - diseq_chain - - - - - - - - - - - - - - - - diseq_chain - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/drop_coercions.xsl b/helm/style/drop_coercions.xsl deleted file mode 100644 index 7b1316013..000000000 --- a/helm/style/drop_coercions.xsl +++ /dev/null @@ -1,184 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/expandobj.xsl b/helm/style/expandobj.xsl deleted file mode 100644 index 6c61823d8..000000000 --- a/helm/style/expandobj.xsl +++ /dev/null @@ -1,85 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/genmmlid.xsl b/helm/style/genmmlid.xsl deleted file mode 100644 index c4981c5d6..000000000 --- a/helm/style/genmmlid.xsl +++ /dev/null @@ -1,55 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/getter.xsl b/helm/style/getter.xsl deleted file mode 100644 index c2f36de5c..000000000 --- a/helm/style/getter.xsl +++ /dev/null @@ -1,34 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - getxml?uri= - - - diff --git a/helm/style/headercontent.xsl b/helm/style/headercontent.xsl deleted file mode 100644 index add3247b3..000000000 --- a/helm/style/headercontent.xsl +++ /dev/null @@ -1,47 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/html_init.xsl b/helm/style/html_init.xsl deleted file mode 100644 index 91d978f5c..000000000 --- a/helm/style/html_init.xsl +++ /dev/null @@ -1,507 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ??? - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ??? - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ( - - - - - - - - - - - - - - - - - ) - - - - - - - - - - - - - - - - - - - - - - - - - - ( - - - - - - - - - - - - - - - - - ) - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - : - - . - - - - - - - - - - - - - - - - - ( - - - -
- - - - - - - - - - - - - - - - - - - - - ) -
- - - -
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ( - - - -
- - - - - - - - - - - - - - - - - - - - - ) -
- - - -
-
-
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - : - - - -
- - - - . - - - -
- - - -
-
- - - - - - - - - - - - - - - - - - - - - - - - -
diff --git a/helm/style/html_reals.xsl b/helm/style/html_reals.xsl deleted file mode 100644 index a78f454bd..000000000 --- a/helm/style/html_reals.xsl +++ /dev/null @@ -1,469 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ??? - - - - - - - - - - - - - - - - - - ??? - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - lim - - - - lim - - - - - - - - - - - - - - - - - - - - d - / - - d - - - - - - d - / - - d - - - - - - - - - - - - - | - - | - - - - - - - - - - ! - - - - - - - - - (sqr - - ) - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - { - - , - - } - - - - - - - - - - - - - - - - - - - - - - - lim - - - - lim - - - - - - - - - -
- - - - - - -
- - - -
-
- - - - - - - - - - d - / - - d - - - - - - d - / - - d - - - - - - - - - - - - - - - - - - | - - - - | - - - - - - - - - - - - - - ! - - - - - - - - - - - (sqr - - - - ) - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - { - - - - , -
- - - - - - - } -
- - - -
-
- - - - - - - - - - - - - - - - - - - - - - - -
diff --git a/helm/style/html_set.xsl b/helm/style/html_set.xsl deleted file mode 100644 index 4003d258c..000000000 --- a/helm/style/html_set.xsl +++ /dev/null @@ -1,389 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - { - - : - - | - - } - - - { - - - - - } - - - , - - - - - - - - - - - - - - - - - - | - - | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ( - - - - - - - - - - - - - - - - - - - - - ) - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ( - - - -
- - - - - - - - - - - - - - - - - - - - - - - - - ) -
- - - -
-
- - - - - - - - - - - - - - - - - - - - - - - { - - : - - -
- - - - | - - - - } -
- - { - - - - - , -
- - - - - - -
- } -
-
-
- - - -
-
-
-
- - - - - - - - - | - - - - | - - - - - - - - - - - - - - - - - - - - - - - - -
diff --git a/helm/style/inductive.xsl b/helm/style/inductive.xsl deleted file mode 100644 index 1d6dc4dd7..000000000 --- a/helm/style/inductive.xsl +++ /dev/null @@ -1,416 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - by_induction - - - - - - - - - - - inductive_case - - case_lhs - - - - - - - - - - - induction_hypothesis - - - - - - - - - - - - - - - - - - - - - - - - - extra_args - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/ite.xsl b/helm/style/ite.xsl deleted file mode 100644 index 1b0e14a72..000000000 --- a/helm/style/ite.xsl +++ /dev/null @@ -1,48 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ite - - - - - - - - - diff --git a/helm/style/lambda.xsl b/helm/style/lambda.xsl deleted file mode 100644 index 28c876fa0..000000000 --- a/helm/style/lambda.xsl +++ /dev/null @@ -1,158 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - subst - - - - - - - - - subst - - - 0 - - - - - - - lift_with_base - - - - - - - - - lift - - - - - - - - - beta_red1 - - - - - - - - beta_red - - - - - - - - par_beta_red1 - - - - - - - - par_beta_red - - - - - - - - - - forgetful - - - - - - - - - - - - - - - - - - - - - - - - - - - - - isomorphic - - - - - - - - - - - - - - - - - - diff --git a/helm/style/link.xsl b/helm/style/link.xsl deleted file mode 100644 index e6d639a3b..000000000 --- a/helm/style/link.xsl +++ /dev/null @@ -1,127 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - other - - - - - - - - - - - - - - - - - - - - - - - - cic - - - - - - - - theory - - - - - - - - - - _blank - - - - - - - - - - - - - - diff --git a/helm/style/links_library.xsl b/helm/style/links_library.xsl deleted file mode 100644 index 22e0ac48d..000000000 --- a/helm/style/links_library.xsl +++ /dev/null @@ -1,363 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - getxml?uri= - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -?url= -?url= -apply?keys= -&param.naturalLanguage=&param.proofcheckerURL=&param.draw_graphURL=&param.uri_set_queueURL=&param.UNICODEvsSYMBOL=&param.annotations=&prop.doctype-public=&param.doctype-public=&param.encoding=&param.media-type=&param.keys=&param.getterURL=&param.processorURL=&param.interfaceURL=&param.topurl=&xmluri= -&prop.media-type=&prop.encoding= -&prop.media-type=&param.thmedia-type=&param.thkeys=&param.embedkeys=&param.thinterfaceURL=&param.thencoding=&prop.encoding= - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - %23 - - - - - %26param.CICURI%3D - - - - - - - - - - - - - - - - - - - %23 - - - - - %26param.CICURI%3D - - - - - - - - - - - - - - - - - - - - - - - %23 - - - - - - - - &param.CICURI=&param.type= - - - - - - - - - - - - - - - - - - - - - %23 - - - - d_c&param.getterURL=&param.CICURI=&xmluri= - - - - diff --git a/helm/style/logic.xsl b/helm/style/logic.xsl deleted file mode 100644 index 0a261260a..000000000 --- a/helm/style/logic.xsl +++ /dev/null @@ -1,155 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - false_ind - cic:/Coq/Init/Logic/False_ind.con - - - - - - - - - and_ind - - - - - - - - - - - - - - - - - - - - - full_or_ind - - - - - - left_case - - - - - - - - - - - - right_case - - - - - - - - - - - - - - - - - - - - ex_ind - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/mk_dep_graph.xsl b/helm/style/mk_dep_graph.xsl deleted file mode 100644 index 4cdc17f35..000000000 --- a/helm/style/mk_dep_graph.xsl +++ /dev/null @@ -1,38 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/mk_meta_and_dep_graph.xsl b/helm/style/mk_meta_and_dep_graph.xsl deleted file mode 100644 index c860e4b46..000000000 --- a/helm/style/mk_meta_and_dep_graph.xsl +++ /dev/null @@ -1,265 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - strict digraph L0 { size = "83,83"; node [style=filled, shape = box]; - - - - - - - - - - - } - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - [label=" - - ",URL=" - - " - - ,color=red - - ]; - - - - - - - - - - - - - - - - - - - - - -> - - - ; - - - - - diff --git a/helm/style/mk_meta_graph.xsl b/helm/style/mk_meta_graph.xsl deleted file mode 100644 index aecf9ef3e..000000000 --- a/helm/style/mk_meta_graph.xsl +++ /dev/null @@ -1,38 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/mk_meta_theory.xsl b/helm/style/mk_meta_theory.xsl deleted file mode 100644 index e433c4b26..000000000 --- a/helm/style/mk_meta_theory.xsl +++ /dev/null @@ -1,171 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - Occurrences of <xsl:value-of select="*/*/@rdf:about"/> - - - - - - - - - - - - - - - - -

Occurrences of

- - - - - -

Head position inside conclusion:

- -
- -
-
-
- -

Head position inside conclusion:

- -
- -
-
-
-
- - - -

Inside conclusion:

- -
- -
-
-
- -

Inside conclusion:

- -
- -
-
-
-
- - - -

Head position inside an hypothesis:

- -
- -
-
-
- -

Head position inside an hypothesis:

- -
- -
-
-
-
- - - -

Inside an hypothesis:

- -
- -
-
-
- -

Inside an hypothesis:

- -
- -
-
-
-
- -

Inside the body:

- -
- -
-
-
-
- -
diff --git a/helm/style/mmlctop.xsl b/helm/style/mmlctop.xsl deleted file mode 100644 index b63ebee8a..000000000 --- a/helm/style/mmlctop.xsl +++ /dev/null @@ -1,4005 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - e - - - - - - - - - - - - - + - - - - i - - - - - - - - - - - - - + - - - - i - - - - - - - - - - - - - - - - - - - - - - - - Polar - - - - - - - - - - - Polar - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - i - - - - - - - - - - - - - + - - - - i - - - - - - - - - - - - - - - - - - - - - - - - Polar - - - - - - - - - - - Polar - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - [ - - - ] - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -1 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - Λ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - id - - - id - - - - - - - - - - - - - { - - - - - - - - - - - - if - - - - - - - - - - - - - - - otherwise - - - - - - - - - - - - - - - - - - domain - - - - - - - - - - - - - - - codomain - - - - - - - - - - - - - - - image - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - e - - - - - - - - - - - - - - - - - - - - - - ! - - - - - - - - - - - - - - - - - - - - max - - - - - - - - - min - - - - - - - - - - - | - - - - - - - - - - - - - - - - - - - - max - - - - - - - - - min - - - - - - - - - | - - - - - - - - - - - - - max - - - - - - - - - min - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - * - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 2 - - - - - - - - - - - - - - - - - - - gcd - - - - - - - - - - gcd - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ¬ - - - - - - - - - - - - - - - - - - - - for all - - - - - - - - - - - - : - - , - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - , - - - - : - - - - - - - - - - - - - - - - - - - - - - | - - - - - - - - | - - - - - - - - - - - - - - - - - - - | - - - - - - - - | - - - - - - - - - - - - - - - - - - - - - - - - ̲ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - lcm - - - - - - - - - - lcm - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ln - - - - - - - - - - - ln - - - - - - - - - - - - - - - - - - - - - - - - - - - log - - - - - - - - - - - - log - - - - - - - - - - - - - - log - - - - - - - - - - log - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - d - - - - d - - - - - - - - - - - - - - - - d - - d - - - - - - - - - - - - - - - - - - - - - - - - - - d - - - - d - - - - - - - - - - - - - - - - d - - d - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - Δ - 2 - - - - - - - - - - - - - - - - - - | - - - - - - - - - | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - \ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - × - - - - - - - - - - - - - - - - - - - - - - - - - | - - - - - - - - - - | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - = - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - d - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - d - - - - - - - - - - - - - - - - - - d - - - - - - - - - - - - - d - - - - - - - - - - - - - - - - - - - - - - lim - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - < - - - - , - - - - - - - - - - > - - - - - - - - - - - - - - - - - - - σ - - - - - - - - - - - - - - - - - - - - - - - σ - - - - - - - 2 - - - - - - - - - - - - - - - - - - median - - - - - - - - - - - - - - - - - - - - - - mode - - - - - - - - - - - - - - - - - - - - - - - - < - - - - - - - - - - - - - - - - - - - - - - - - - - - - - > - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - det - - - - - - - - - - - - - - - - - - - T - - - - - - - - - - - - - - - - - - - - - - - - - - * - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - NaN - - - - - - - - - - true - - - - - - - - - - false - - - - - - - - - - - - - - - - - - - - - - - - π - - - - - - - - - - - - γ - - - - - - - - - - - - - - - - - diff --git a/helm/style/mmlctop.xsl-0.14 b/helm/style/mmlctop.xsl-0.14 deleted file mode 100755 index 1568e1da2..000000000 --- a/helm/style/mmlctop.xsl-0.14 +++ /dev/null @@ -1,3103 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - i - - - - - - - - - - - - - + - - - - i - - - - - - - - - - - - - - - - - - - - - - - - Polar - - - - - - - - - - - Polar - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - i - - - - - - - - - - - - - + - - - - i - - - - - - - - - - - - - - - - - - - - - - - - Polar - - - - - - - - - - - Polar - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - [ - - - ] - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -1 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - Λ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - id - - - id - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - e - - - - - - - - - - - - - - - - - - - - - - ! - - - - - - - - - - - - - - - - - - - - max - - - - - - - - - min - - - - - - - - - - - | - - - - - - - - - - - - - - max - - - min - - - - - - - - - | - - - - - - - max - - - min - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - * - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 2 - - - - - - - - - - - - - - - - - - - gcd - - - - - - - - - - gcd - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ¬ - - - - - - - - - - - - - - - - - - - - for all - - - - - - - - - - - - : - - , - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - , - - - - : - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ̲ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ≠ - - - - - - - - - ≊ - - - - - - - - - → - - - - - - - - - ⇒ - - - - - - - - - ∈ - - - - - - - - - ∉ - - - - - - - - - ⊄ - - - - - - - - - ⊈ - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - ⊆ - - - - - - - - - ⊂ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ≥ - - - - - - - - - ≤ - - - - - - - - - ≡ - - - - - - - - - - - - - - - - - - - - - - - - - - - - ln - - - - - - - - - - - ln - - - - - - - - - - - - - - - - - - - - - - - - - - - log - - - - - - - - - - - - log - - - - - - - - log - - - - - - - - - - log - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - d - - - - d - - - - - - - - - - - - - - - - d - - d - - - - - - - - - - - - - - - - - - - - - - - - - - d - - - - d - - - - - - - - - - - - - - - - d - - d - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - Δ - 2 - - - - - - - - - - - - - - - - - - | - - - - - - - - - | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - \ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ∑ - - - - - - - - - ∏ - - - - - = - - - - - - - - - - - - - - - - - ∑ - - - - - - - - - ∏ - - - - - - - - - - - - - - - - - - - - - - - - - lim - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - σ - - - - - - - - - - - - - - - - - - - - - - σ - - - - - - - 2 - - - - - - - - - - - - - - - - - - median - - - - - - - - - - - - - - - - - - - - - - mode - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - det - - - - - - - - - - - - - - - - - - - T - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ⨯ - - - - - - - - - - - - - - - - diff --git a/helm/style/mmlctop2_0.xsl b/helm/style/mmlctop2_0.xsl deleted file mode 100644 index 554c3a87b..000000000 --- a/helm/style/mmlctop2_0.xsl +++ /dev/null @@ -1,3985 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - e - - - - - - - - - - - - - + - - - - i - - - - - - - - - - - - - + - - - - i - - - - - - - - - - - - - - - - - - - - - - - - Polar - - - - - - - - - - - Polar - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - i - - - - - - - - - - - - - + - - - - i - - - - - - - - - - - - - - - - - - - - - - - - Polar - - - - - - - - - - - Polar - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - [ - - - ] - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -1 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - Λ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - id - - - id - - - - - - - - - - - - - { - - - - - - - - - - - - if - - - - - - - - - - - - - - - otherwise - - - - - - - - - - - - - - - - - - domain - - - - - - - - - - - - - - - codomain - - - - - - - - - - - - - - - image - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - e - - - - - - - - - - - - - - - - - - - - - - ! - - - - - - - - - - - - - - - - - - - - max - - - - - - - - - min - - - - - - - - - - - | - - - - - - - - - - - - - - - - - - - - max - - - - - - - - - min - - - - - - - - - | - - - - - - - - - - - - - max - - - - - - - - - min - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - * - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 2 - - - - - - - - - - - - - - - - - - - gcd - - - - - - - - - - gcd - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ¬ - - - - - - - - - - - - - - - - - - - - for all - - - - - - - - - - - - : - - , - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - , - - - - : - - - - - - - - - - - - - - - - - - - - - - | - - - - - - - - | - - - - - - - - - - - - - - - - - - - | - - - - - - - - | - - - - - - - - - - - - - - - - - - - - - - - - ̲ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - lcm - - - - - - - - - - lcm - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ln - - - - - - - - - - - ln - - - - - - - - - - - - - - - - - - - - - - - - - - - log - - - - - - - - - - - - log - - - - - - - - - - - - - - log - - - - - - - - - - log - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - d - - - - d - - - - - - - - - - - - - - - - d - - d - - - - - - - - - - - - - - - - - - - - - - - - - - d - - - - d - - - - - - - - - - - - - - - - d - - d - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - Δ - 2 - - - - - - - - - - - - - - - - - - | - - - - - - - - - | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - \ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - × - - - - - - - - - - - - - - - - - - - - - - - - - | - - - - - - - - - - | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - = - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - d - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - d - - - - - - - - - - - - - - - - - - d - - - - - - - - - - - - - d - - - - - - - - - - - - - - - - - - - - - - lim - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - < - - - - , - - - - - - - - - - > - - - - - - - - - - - - - - - - - - - σ - - - - - - - - - - - - - - - - - - - - - - - σ - - - - - - - 2 - - - - - - - - - - - - - - - - - - median - - - - - - - - - - - - - - - - - - - - - - mode - - - - - - - - - - - - - - - - - - - - - - - - < - - - - - - - - - - - - - - - - - - - - - - - - - - - - - > - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - det - - - - - - - - - - - - - - - - - - - T - - - - - - - - - - - - - - - - - - - - - - - - - - * - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - NaN - - - - - - - - - - true - - - - - - - - - - false - - - - - - - - - - - - - - - - - - - - - - - - π - - - - - - - - - - - - γ - - - - - - - - - - - - - - - - - diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl deleted file mode 100644 index fad3dce6b..000000000 --- a/helm/style/mmlextension.xsl +++ /dev/null @@ -1,2382 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - DEFINITION () OF TYPE - - - - - - - __ - - - - - - - - AS - - - - - - - __ - - - - - - - - - - - - - - - - - AXIOM () OF TYPE - - - - - - - __ - - - - - - - - - - - - - - - - - UNFINISHED PROOF () - - - - - - - THESIS: - - - - - - - __ - - - - - - - - CONJECTURES: - - - - - - - - __ - - - - - - - - - - _ - - - : - - - - - - - - - - - _ - - - := - - - - - - _ - :? - _ - - - - - ; - - - |- - ? - : - - - - - - - - - PROOF: - - - - - - - __ - - - - - - - - - - - - - - - - - - - - - - INDUCTIVE DEFINITION - - - COINDUCTIVE DEFINITION - - - - - AND - - - _ - () - - - - - - - __ - [ - - - - - - - - - : - - - - - - - - - ] - - - - - - - ] - - - - - - - - - OF ARITY - - - - - - - __ - - - - - - - - BUILT FROM - - - - - - - - - - __ - - - | - _ - - - OF - _ - - - - - - - - - - - - - - - - - - - VARIABLE OF TYPE - - - - - - - __ - - - - - - - - - AS - - - - - - - __ - - - - - - - - - - - - - - - - none - - - solid - - - - ? - : - _ - - - - - - - - - : - - - := - - - - - - - - - - - - _ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - : - - - - - - - - - - - - - - - - : - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - . - - - - - - - - - - : - - . - - - - - - - - - - - - - LET - _ - - - - - - - - = - - - - - - - - IN - _ - - - - - - - - LET - _ - - = - - _ - IN - _ - - - - - - - - - - - - - Π - - - - - - - - . - - - - - - - - Π - - : - - . - - - - - - - - - - - - - - ( - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ) - - - - - - - - - ( - - - - - - - - - - - - - - - - - - - - - ) - - - - - - - - - - - - - ( - - - - - - - - - - - - ( - - - - - - - - - - - - ) - - - - - - - ( - - - - - - _ - - - - - - ) - - - - - - - - - - - - ( - - - - - - - - :> - - - - - - - - ) - - - - - - - ( - - :> - - ) - - - - - - Prop - - - - Set - - - - Type - - - - - - - - - - - < - - - > - CASES - _ - - - - - - - - - - > - CASES - _ - - - - - - - - - OF - - - - - - - - - - - | - - - | - - - _ - - - - - - - - - - - - - |_ - - - - - - - - - - - END - - - - - - - <> - CASES - _ - - _ - OF - - - - | - - - - - - - _ - END - - - - - - - - - - - - FIX - _ - - { - - - - - - - __ - - - - - - - - : - - - - - - - - - - - := - - - - - - - - - := - - - - - - - - - - - - - } - - - - - - - FIX - - { - - - - - - - : - - := - - - } - - - - - - - - - - - - - - - - - - COFIX - _ - - { - - - - - - - __ - - - - - - - - : - - - - - - - - - - - := - - - - - - - - - := - - - - - - - - - - - - - } - - - - - - - COFIX - - { - - - - - - - : - - := - - - } - - - - - - - - - - - - - - - - - { - - - := - - - } - - - - - - - - - - - - @ - - - - - - - - - - - - - - - - @ - - - - - - - - - - - - - - if - - - - - - - - then - - - - - - - - else - - - - - - - - - if - - then - - else - - - - - - - - - - - - - - - - - - - - We can prove - _ - - - - - _ - (explain) - - - - - - - - - - - - - - - - - - - - - _ - - - (hide details) - - - - - - - we proved - _ - - - - - - - - - - - - that is equivalent to - _ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - We can prove - _ - - - - - _ - (explain) - - - - - - - - - - - - - - - - - - - - - _ - - - (hide details) - - - - - - - we proved - _ - - - - - - - - - - - - that is equivalent to - _ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - We prove - _ - - - - - - - - by induction on - _ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - Case - _ - - - - - - - - _ - - - - - - By induction hypothesis, we have: - - - - - - - _ - - ( - - ) - _ - - - - - - - - - - - - - - - - - - - - - - - - - - - - ( - - - _ - - : - - - ) - - - - - - - - - - - - - - - - - - Contradiction. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ( - - ) - - - - - - - - - - - - - - Consider - _ - - - - - - - - - - - - - - - - - - - - - - - Rewrite - _ - - - - - - - - - - with - _ - - - - - - - - by - _ - - - - - - - - - - with - _ - - _ - by - _ - - - - - - - - - - - - Rewrite - _ - - _ - with - _ - - - - - - - - by - _ - - - - - - - - - - Rewrite - _ - - _ - with - _ - - _ - by - _ - - - - - - - - - - - - - - - - - - - - - - - Then apply it to - _ - - - - - - - - - - - - - - - - - - Consider - _ - - - - - - - - - - In particular, we have - - - - - - - ( - - ) - _ - - - - - - - - ( - - ) - _ - - - - - - - - - - - - - - - - - - - - - - - - - Consider - _ - - - - - - - - - - We proceed by cases to prove - _ - - - - - - - - Left: suppose - _ - ( - - ) - _ - - - - - - - - _ - - - - - - - - Right: suppose - _ - ( - - ) - _ - - - - - - - - - - - - - - - - - - - - - - - - - Consider - _ - - - - - - - - - - We prove - _ - - _ - by cases: - - - - - - - Left - - - - - - - - Right - - - - - - - - - - - - - - - - - - Consider - _ - - - - - - - - - - Let - _ - - : - - _ - such that - _ - ( - - ) - _ - - - - - - - - - - - - - - - - - - - - We have the following equality chain: - - - - - - - - - - - - _ - = - - - = - _ - - - - - - - - - - - __ - - - - - - - - - - - - - - - We have the following disequality chain: - - - - - - - - - - - - _ - - - - - _ - - - - - - - - - - - __ - - - - - - - - - - - - - - - - [ - - - - - - - ] - - - - - - - - - - - - ( - - ) - - - - - - - - - - - - - - ( - - ) - - - - - - - - - - - β - - - - - - - - - - - - β - * - - - - - - - - - - - - β - - - - - - - - - - - - β - * - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ERROR("") - - - - - - - - - - - - - - - - - - - - - - - - λ - - - - - - - - . - - - - - - - - λ - - : - - . - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 3 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/mmlnotation.xsl b/helm/style/mmlnotation.xsl deleted file mode 100644 index 7081ad83f..000000000 --- a/helm/style/mmlnotation.xsl +++ /dev/null @@ -1,397 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ( - - - - - - - - - __ - - - - - - = - - - - - - - - - ) - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ( - - - - - - - - __ - - - - - - - - - - - - - - ) - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ( - - - - - - - - - __ - - - - - - - - - - - - - - - ) - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - { - - - - - - - - { - | - - - - - - - - - - - - - } - - - - - - - - - - - - - - - - { - - - , - - - - - - - - - { - - - , - - - - - - - - - - - - - - } - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/mmltheoryextension.xsl b/helm/style/mmltheoryextension.xsl deleted file mode 100644 index d173c795d..000000000 --- a/helm/style/mmltheoryextension.xsl +++ /dev/null @@ -1,42 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/objcontent.xsl b/helm/style/objcontent.xsl deleted file mode 100644 index 5b243e783..000000000 --- a/helm/style/objcontent.xsl +++ /dev/null @@ -1,242 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - click here - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/objtheorycontent.xsl b/helm/style/objtheorycontent.xsl deleted file mode 100644 index 5bad7e108..000000000 --- a/helm/style/objtheorycontent.xsl +++ /dev/null @@ -1,85 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/params.xsl b/helm/style/params.xsl deleted file mode 100644 index 1b5f41670..000000000 --- a/helm/style/params.xsl +++ /dev/null @@ -1,430 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 0 - - - - - - - - - - - - - - - - - - - - - - - - 0 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -PROD - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - app - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - $ - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl deleted file mode 100644 index dbcfabaa3..000000000 --- a/helm/style/proofs.xsl +++ /dev/null @@ -1,559 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - yes - - - - - - - - proof - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - yes - - - - - - - proof - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - yes - - - - - - - proof - - let_in - - - - - - - - - - - - - - - - let_in - - - - - - - - - - - - - - - - - - - - - - - proof - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - let_in - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - proof - - - side_proof - - - - - - - - - - - - - - - - - - - - - yes - - - - - - * - - - - - - - - - - letin1 - - - - - - yes - - - - - - - - - - app - - - - - - - - letin - - - - - app - - - - - - - - - - app - - - - - - - - - - - - - - - - - - - - - - - - - - yes - - - - - - - let - - - - - - - - - - - - - - - - - - - - - - - - - - - - . - - - - - - - - - - - yes - - - - - - previous - - - - - - - - - . - - - - - - - - - - - - - - - yes - - - - - - - - - - - - - - - - - - - . - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/rewrite.xsl b/helm/style/rewrite.xsl deleted file mode 100644 index e361944d3..000000000 --- a/helm/style/rewrite.xsl +++ /dev/null @@ -1,135 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - rw_step - - - - - - - - - - - - - - - rewrite_and_apply - - rw_step - - - - - - - - - - - - - - - letin - - let - - - - - - - - - - - - - rewrite_and_apply - - rw_step - - - - - - - - - - - - - - - - - - - - - - letin - - - - - - rewrite_and_apply - - rw_step - - - - - - - - - - - - - - - - - - - - - \ No newline at end of file diff --git a/helm/style/ricerca.xsl b/helm/style/ricerca.xsl deleted file mode 100644 index d665eac51..000000000 --- a/helm/style/ricerca.xsl +++ /dev/null @@ -1,104 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -getxml?uri= - - - - - - - - - - - - - - - - - - - - - - - - - - -
-
-
- - - -

- - - - - - - - -
- - - - - - - - - - - - - - - - - - - - - - - - -
diff --git a/helm/style/ring.xsl b/helm/style/ring.xsl deleted file mode 100644 index 5136e77d5..000000000 --- a/helm/style/ring.xsl +++ /dev/null @@ -1,134 +0,0 @@ - - - - - - - - - app - - ... - - - - - - - - - - - - - - - - - - - - - - - - - - - app - - - - - - - - - - - - - - - - - - ERROR INTERP: - - - - - - - - - - - - - - - - 0 - - - - - 1 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/rootcontent.xsl b/helm/style/rootcontent.xsl deleted file mode 100644 index addef615b..000000000 --- a/helm/style/rootcontent.xsl +++ /dev/null @@ -1,94 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/roottheory.xsl b/helm/style/roottheory.xsl deleted file mode 100644 index 023190b0d..000000000 --- a/helm/style/roottheory.xsl +++ /dev/null @@ -1,44 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/show_dc.xsl b/helm/style/show_dc.xsl deleted file mode 100644 index 56f7957aa..000000000 --- a/helm/style/show_dc.xsl +++ /dev/null @@ -1,249 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

Dublin Core Metadata for :

- - - -
- - -

No Dublin Core Metadata available for .

-
-
-
- - - - - - - - - - - - -
- - - - - - - - - - - - - - - - - - - -
-
- - - - Title: - - - - - - - Creator: - - - - - - - Contributor: - - - - - - - Subject: - - - - - - - Description: - - - - - - - Publisher: - - - - - - - Date: - - - - - - - Coverage: - - - - - - - Type: - - - - - - - - - - - Format: - - - - - - - - - - - Identifier: - - - - - - - Source: - - - - - - - Language: - - - - - - - Relation: - - - - - - - - - - - - - Rights: - - - - - - - Institution: - - - - - - - Contact: - - - - - - - First Version: - - - - - - - Modified: - - - - - - - ERROR! - - - - -
diff --git a/helm/style/theory_content.xsl b/helm/style/theory_content.xsl deleted file mode 100644 index e3e50b1f1..000000000 --- a/helm/style/theory_content.xsl +++ /dev/null @@ -1,90 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/style/theory_pres.xsl b/helm/style/theory_pres.xsl deleted file mode 100644 index 47b2622c8..000000000 --- a/helm/style/theory_pres.xsl +++ /dev/null @@ -1,127 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

BEGIN MUTUAL DEFINITIONS

- -

END MUTUAL DEFINITIONS

-
- - - - - : - - - - - - - - - - - - -
- Object  -
   
-
- - - - - - - - - - -
-  : -
   
-
- - - - - - - - - - -
-  : -
   
-
- - -Inductive DefinitionCoInductive DefinitionRecord DefinitionDefinition - - - - - - - - -
-  : -
   
-
- - - - - - - - - - -
diff --git a/helm/style/xslt_index.txt b/helm/style/xslt_index.txt deleted file mode 100644 index 84cd46836..000000000 --- a/helm/style/xslt_index.txt +++ /dev/null @@ -1,40 +0,0 @@ -annotatedcont.xsl -annotatedpres.xsl -content.xsl -content_to_html.xsl -contentlib.xsl -diseq.xsl -drop_coercions.xsl -expandobj.xsl -genmmlid.xsl -getter.xsl -headercontent.xsl -html_init.xsl -html_reals.xsl -html_set.xsl -inductive.xsl -ite.xsl -lambda.xsl -link.xsl -links_library.xsl -logic.xsl -mk_dep_graph.xsl -mk_meta_and_dep_graph.xsl -mk_meta_graph.xsl -mk_meta_theory.xsl -mmlctop.xsl -mmlextension.xsl -mmlnotation.xsl -mmltheoryextension.xsl -objcontent.xsl -objtheorycontent.xsl -params.xsl -proofs.xsl -rewrite.xsl -ricerca.xsl -ring.xsl -rootcontent.xsl -roottheory.xsl -show_dc.xsl -theory_content.xsl -theory_pres.xsl -- 2.39.2