From: no author Date: Thu, 21 Nov 2002 16:58:01 +0000 (+0000) Subject: This commit was manufactured by cvs2svn to create branch X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5379335718a93d3e933d9bfdc0dd85f00983bc21;p=helm.git This commit was manufactured by cvs2svn to create branch 'V7_3_new_exportation'. --- diff --git a/helm/meta_style/.cvsignore b/helm/meta_style/.cvsignore new file mode 100644 index 000000000..b88948804 --- /dev/null +++ b/helm/meta_style/.cvsignore @@ -0,0 +1,5 @@ +algebra.xsl +arith.xsl +basic.xsl +reals.xsl +set.xsl diff --git a/helm/meta_style/Makefile b/helm/meta_style/Makefile new file mode 100644 index 000000000..7bb47374d --- /dev/null +++ b/helm/meta_style/Makefile @@ -0,0 +1,56 @@ +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 + +clean: + rm -f algebra.xsl arith.xsl basic.xsl reals.xsl set.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 diff --git a/helm/meta_style/algebra.xml b/helm/meta_style/algebra.xml new file mode 100644 index 000000000..119effa3d --- /dev/null +++ b/helm/meta_style/algebra.xml @@ -0,0 +1,204 @@ + + + + + + + + 0 + + + + 1 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + app + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/meta_style/arith.xml b/helm/meta_style/arith.xml new file mode 100644 index 000000000..17fc523cd --- /dev/null +++ b/helm/meta_style/arith.xml @@ -0,0 +1,69 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/meta_style/basic.xml b/helm/meta_style/basic.xml new file mode 100644 index 000000000..8b4c24520 --- /dev/null +++ b/helm/meta_style/basic.xml @@ -0,0 +1,77 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/meta_style/meta_cic2mathml.xsl b/helm/meta_style/meta_cic2mathml.xsl new file mode 100644 index 000000000..005821e6f --- /dev/null +++ b/helm/meta_style/meta_cic2mathml.xsl @@ -0,0 +1,1314 @@ + + + + + + + + + + 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 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + *[2]/ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + $no_params + + + + + + + + + + + + + *[2]/ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + CONST[@uri='cic:/Coq/Init/Logic/not.con'] and + + + + + + + + + + APPLY[ + + ] + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + {@id} + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + {@id} + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + app + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + /target/@binder + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + CONST + MUTIND + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + *[2]/ + + + + $no_params+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + APPLY/ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + {@id} + + + + @id + @uri + + + + + + + + + + + + + + + + + diff --git a/helm/meta_style/modeset.xsl b/helm/meta_style/modeset.xsl new file mode 100644 index 000000000..9c0af40ea --- /dev/null +++ b/helm/meta_style/modeset.xsl @@ -0,0 +1,65 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/meta_style/operator.dtd b/helm/meta_style/operator.dtd new file mode 100644 index 000000000..c76466956 --- /dev/null +++ b/helm/meta_style/operator.dtd @@ -0,0 +1,71 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/meta_style/positive.xsl b/helm/meta_style/positive.xsl new file mode 100644 index 000000000..f52b64702 --- /dev/null +++ b/helm/meta_style/positive.xsl @@ -0,0 +1,177 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 0 + + + + + + + + + + + + + + 1 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/meta_style/reals.xml b/helm/meta_style/reals.xml new file mode 100644 index 000000000..b4cdf2d8a --- /dev/null +++ b/helm/meta_style/reals.xml @@ -0,0 +1,163 @@ + + + + + + + + 0 + + + + 1 + + + + + + + + + + + + + 2 + + + + + + + + + + 1 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/meta_style/set.xml b/helm/meta_style/set.xml new file mode 100644 index 000000000..9384b8430 --- /dev/null +++ b/helm/meta_style/set.xml @@ -0,0 +1,315 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/meta_style/subst.pl b/helm/meta_style/subst.pl new file mode 100755 index 000000000..27ca245d5 --- /dev/null +++ b/helm/meta_style/subst.pl @@ -0,0 +1,17 @@ +#!/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 new file mode 100644 index 000000000..889ce4c6c --- /dev/null +++ b/helm/meta_style/xslt_index.txt @@ -0,0 +1,7 @@ +algebra.xsl +arith.xsl +basic.xsl +reals.xsl +set.xsl +positive.xsl +modeset.xsl