From: Claudio Sacerdoti Coen Date: Mon, 19 Jan 2004 15:13:45 +0000 (+0000) Subject: Branch V7_3_new_exportation merged. X-Git-Tag: V_0_5_1_3~19 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5f2de2d1d6c8520e39c1c3793a4c2776dcf7c7c1;p=helm.git Branch V7_3_new_exportation merged. --- diff --git a/helm/meta_style/.cvsignore b/helm/meta_style/.cvsignore index b88948804..b20cfb281 100644 --- a/helm/meta_style/.cvsignore +++ b/helm/meta_style/.cvsignore @@ -3,3 +3,4 @@ arith.xsl basic.xsl reals.xsl set.xsl +list.xsl diff --git a/helm/meta_style/Makefile b/helm/meta_style/Makefile index c0e5fc645..f51cc8094 100644 --- a/helm/meta_style/Makefile +++ b/helm/meta_style/Makefile @@ -1,14 +1,14 @@ XSLTPROC = xsltproc --timing FORMAT = xmllint --format SUBST = ./subst.pl -METASTYLESHEET = meta_cic2mathml.xsl -TMP1 = /tmp/.tmpfile1 -TMP2 = /tmp/.tmpfile2 +METASTYLESHEET = ./meta_cic2mathml.xsl +TMP1 = .tmpfile1 +TMP2 = .tmpfile2 -all: algebra.xsl arith.xsl basic.xsl reals.xsl set.xsl +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 + rm -f algebra.xsl arith.xsl basic.xsl reals.xsl set.xsl list.xsl algebra.xsl: algebra.xml $(METASTYLESHEET) @echo "**** PROCESSING algebra.xml ****" @@ -54,3 +54,12 @@ set.xsl: set.xml $(METASTYLESHEET) @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 index 119effa3d..696a19a1b 100644 --- a/helm/meta_style/algebra.xml +++ b/helm/meta_style/algebra.xml @@ -1,33 +1,34 @@ - + 0 1 @@ -36,63 +37,63 @@ @@ -100,14 +101,14 @@ @@ -120,7 +121,7 @@ @@ -135,7 +136,7 @@ @@ -147,7 +148,7 @@ @@ -166,7 +167,7 @@ @@ -185,7 +186,7 @@ diff --git a/helm/meta_style/arith.xml b/helm/meta_style/arith.xml index 17fc523cd..a21a51306 100644 --- a/helm/meta_style/arith.xml +++ b/helm/meta_style/arith.xml @@ -4,8 +4,6 @@ - - @@ -44,7 +42,7 @@ @@ -56,7 +54,7 @@ diff --git a/helm/meta_style/basic.xml b/helm/meta_style/basic.xml index b0681468c..e9da62a62 100644 --- a/helm/meta_style/basic.xml +++ b/helm/meta_style/basic.xml @@ -7,16 +7,27 @@ + + + iff + + + + + @@ -47,7 +58,7 @@ @@ -61,7 +72,7 @@ diff --git a/helm/meta_style/list.xml b/helm/meta_style/list.xml new file mode 100644 index 000000000..9ed07d69b --- /dev/null +++ b/helm/meta_style/list.xml @@ -0,0 +1,60 @@ + + + + + + + + + + + append + + + + + + + + + + + + + + diff --git a/helm/meta_style/meta_cic2mathml.xsl b/helm/meta_style/meta_cic2mathml.xsl index f77890363..072774b5d 100644 --- a/helm/meta_style/meta_cic2mathml.xsl +++ b/helm/meta_style/meta_cic2mathml.xsl @@ -47,6 +47,7 @@ + @@ -79,7 +80,7 @@ - + @@ -93,13 +94,24 @@ - + + + + + + + + + + + + @@ -107,13 +119,24 @@ - + + + + + + + + + + + + @@ -138,14 +161,14 @@ - + - + @@ -168,11 +191,21 @@ - + + + + + + + + + + + @@ -180,11 +213,21 @@ - + + + + + + + + + + + @@ -205,30 +248,26 @@ - - - *[2]/ - - + + - + - + - and count(*) = 2 - + - + @@ -244,60 +283,21 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + @@ -310,40 +310,27 @@ - - $no_params + - - - + + - - and count(*) = 2 - + + and count(*) = 2 + - + *[2]/ - - - - - - - - - - @@ -351,17 +338,9 @@ - - - - - - - - - + @@ -392,7 +371,12 @@ + + + + instantiate/ + @@ -407,7 +391,7 @@ APPLY[ - + ] @@ -416,7 +400,6 @@ - @@ -427,7 +410,6 @@ - @@ -436,7 +418,6 @@ - @@ -445,7 +426,6 @@ - @@ -459,12 +439,13 @@ - {@id} + {@id} + @@ -473,6 +454,7 @@ + @@ -491,8 +473,7 @@ - - + @@ -512,6 +493,7 @@ + @@ -531,7 +513,6 @@ - @@ -541,7 +522,6 @@ - @@ -549,7 +529,6 @@ - @@ -559,7 +538,6 @@ - @@ -572,6 +550,7 @@ + @@ -590,6 +569,7 @@ + @@ -604,6 +584,7 @@ + @@ -623,7 +604,6 @@ - @@ -638,6 +618,7 @@ + @@ -648,6 +629,7 @@ + @@ -661,6 +643,7 @@ + @@ -671,6 +654,7 @@ + @@ -687,6 +671,7 @@ + @@ -706,8 +691,8 @@ + - @@ -715,7 +700,6 @@ - @@ -743,6 +727,7 @@ + @@ -753,6 +738,7 @@ + @@ -771,6 +757,7 @@ + @@ -790,12 +777,11 @@ - - /target/@binder + /decl/@binder @@ -812,11 +798,10 @@ - - + @@ -827,11 +812,10 @@ - - - + + @@ -877,6 +861,8 @@ + + @@ -884,7 +870,6 @@ - @@ -1004,7 +989,6 @@ - @@ -1014,7 +998,6 @@ - @@ -1023,7 +1006,6 @@ - @@ -1035,7 +1017,6 @@ - @@ -1140,29 +1121,26 @@ - *[2]/ - - $no_params+ - - - + + + @@ -1171,12 +1149,14 @@ + + @@ -1187,8 +1167,13 @@ + + + + instantiate/ + APPLY/ @@ -1199,12 +1184,13 @@ - + + @@ -1232,6 +1218,7 @@ + @@ -1265,6 +1252,7 @@ + @@ -1281,10 +1269,11 @@ @uri - + + diff --git a/helm/meta_style/positive.xsl b/helm/meta_style/positive.xsl index f52b64702..e337b663e 100644 --- a/helm/meta_style/positive.xsl +++ b/helm/meta_style/positive.xsl @@ -73,7 +73,7 @@ and @uri='cic:/Coq/Init/Datatypes/nat.ind' and @noConstr='2']"> - + @@ -81,7 +81,7 @@ and @uri='cic:/Coq/Init/Datatypes/nat.ind' and @noConstr='2']"> - + @@ -92,13 +92,13 @@ and @uri='cic:/Coq/Init/Datatypes/nat.ind' and @noConstr='2']"> - + 0 - + @@ -106,7 +106,7 @@ and @uri='cic:/Coq/Init/Datatypes/nat.ind' and @noConstr='2']"> - + 1 @@ -116,7 +116,7 @@ and @uri='cic:/Coq/Init/Datatypes/nat.ind' and @noConstr='2']"> +and @uri='cic:/Coq/ZArith/fast_integer/positive.ind' and @noConstr='1']"> @@ -124,14 +124,14 @@ and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind' and @noConstr +and @uri='cic:/Coq/ZArith/fast_integer/positive.ind' and @noConstr='2']"> - + @@ -173,5 +173,46 @@ and @uri='cic:/Coq/ZArith/fast_integer/fast_integers/positive.ind' and @noConstr + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/meta_style/set.xml b/helm/meta_style/set.xml index f1e888d98..0dbcd3761 100644 --- a/helm/meta_style/set.xml +++ b/helm/meta_style/set.xml @@ -1,12 +1,13 @@ - + @@ -18,7 +19,7 @@ @@ -28,86 +29,95 @@ - - - - - - - + uri = "cic:/Coq/Sets/Ensembles/Empty_set.ind" + cook = "true" + arity = "1"> - + - - + - + + - + + - + - + - + - - + - - - + uri = "cic:/Coq/Sets/Ensembles/Couple.ind" + cook = "true" + arity = "2"> - + - + - + - - + - - - + uri = "cic:/Coq/Sets/Ensembles/Triple.ind" + cook = "true" + arity = "3"> - + - + - + @@ -115,23 +125,25 @@ - - + - - - + uri = "cic:/Coq/Sets/Ensembles/Intersection.ind" + cook = "true" + arity = "2"> - + - + @@ -141,23 +153,25 @@ - - + - - - + uri = "cic:/Coq/Sets/Ensembles/Union.ind" + cook = "true" + arity = "2"> - + - + @@ -167,12 +181,11 @@ - - + @@ -184,7 +197,7 @@ @@ -194,20 +207,23 @@ - - - + uri = "cic:/Coq/Sets/Ensembles/Setminus.con" + cook = "true" + arity = "2"> - + - + @@ -217,15 +233,13 @@ - - + - - - + uri = "cic:/Coq/Sets/Ensembles/Add.con" + cook = "true" + arity = "2"> @@ -233,9 +247,13 @@ - + - + @@ -247,15 +265,13 @@ - - + - - - + uri = "cic:/Coq/Sets/Ensembles/Subtract.con" + cook = "true" + arity = "2"> @@ -263,9 +279,13 @@ - + - + @@ -277,12 +297,11 @@ - - + @@ -297,7 +316,7 @@ diff --git a/helm/meta_style/xslt_index.txt b/helm/meta_style/xslt_index.txt index 889ce4c6c..2f683f28d 100644 --- a/helm/meta_style/xslt_index.txt +++ b/helm/meta_style/xslt_index.txt @@ -3,5 +3,6 @@ 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 index 97f259d67..9cc298f09 100644 --- a/helm/style/annotatedcont.xsl +++ b/helm/style/annotatedcont.xsl @@ -35,9 +35,9 @@ - + - + @@ -51,7 +51,7 @@ - + diff --git a/helm/style/content.xsl b/helm/style/content.xsl index e60a85051..001ff876d 100644 --- a/helm/style/content.xsl +++ b/helm/style/content.xsl @@ -37,6 +37,7 @@ xmlns:helm="http://www.cs.unibo.it/helm"> + @@ -62,63 +63,98 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../] + - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + let_in - + - + + + + + + + - - - - arrow - - - + + + + + + - - forall + + arrow + - prod + + + forall + + + prod + + + + + + + + + + - - - - - - - - - - - - + + + + + + + + cast @@ -126,12 +162,14 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../] + + @@ -140,6 +178,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../] + app @@ -147,6 +186,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../] + @@ -286,6 +365,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../] + diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl index 856fd6971..56231b2bc 100644 --- a/helm/style/content_to_html.xsl +++ b/helm/style/content_to_html.xsl @@ -39,6 +39,7 @@ + @@ -69,6 +70,12 @@ + + + + + + @@ -114,6 +121,12 @@ + + + + + + @@ -215,6 +228,12 @@ +   @@ -311,6 +330,30 @@ ) + + + ( + + + + + + + + ) + + + + ( + + + + + + + + ) + ( @@ -325,7 +368,7 @@ ( - :> + : ) @@ -363,6 +406,23 @@ select="./*[1]"/> + + + + { + + + / + + + + + + + + } + + FIX @@ -407,6 +467,15 @@ + + + if + + then + + else + + @@ -768,6 +837,10 @@ + + + + @@ -854,6 +927,62 @@ + + + + + ( + + + +
+ + + + + + + + + + + + + ) +
+ + + +
+
+ + + + + ( + + + +
+ + + + + + + + + + + + + ) +
+ + + +
+
@@ -1074,6 +1203,29 @@
+ + + if + + + +
+ + + + then + + + +
+ + + + else + + + +
@@ -1089,6 +1241,24 @@   + +
+ + + + we proved  + + + +
+ + + + and by delta equivalence + + + +
\ - we proved\ + we obtain\ \ '); document.to_be_deleted.push(''); @@ -1130,7 +1300,7 @@ - + diff --git a/helm/style/diseq.xsl b/helm/style/diseq.xsl new file mode 100644 index 000000000..dd3650db7 --- /dev/null +++ b/helm/style/diseq.xsl @@ -0,0 +1,336 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 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 index b31160eab..7b1316013 100644 --- a/helm/style/drop_coercions.xsl +++ b/helm/style/drop_coercions.xsl @@ -40,18 +40,18 @@ + (@uri='cic:/Algebra/algebra/CSemiGroups/csg_crr.con' or + @uri='cic:/Algebra/algebra/CMonoids/cm_crr.con' or + @uri='cic:/Algebra/algebra/CGroups/cg_crr.con' or + @uri='cic:/Algebra/algebra/CRings/cr_crr.con' or + @uri='cic:/Algebra/algebra/CFields/cf_crr.con' or + @uri='cic:/Algebra/algebra/COrdFields/cof_crr.con' or + @uri='cic:/Algebra/reals/CReals/crl_crr.con')]]"> + @uri='cic:/Algebra/algebra/CSetoids/CSetoid_functions/csf_fun.con']]"> @@ -84,7 +84,7 @@ + @uri='cic:/Algebra/algebra/CSetoids/CSetoid_functions/csbf_fun.con']]"> @@ -119,7 +119,7 @@ + @uri='cic:/Algebra/algebra/CSetoids/CSetoid_relations_and_predicates/csr_rel.con']]"> @@ -154,7 +154,7 @@ + @uri='cic:/Algebra/algebra/CRings/nat_injection/nring.con']]"> diff --git a/helm/style/headercontent.xsl b/helm/style/headercontent.xsl index f60883079..add3247b3 100644 --- a/helm/style/headercontent.xsl +++ b/helm/style/headercontent.xsl @@ -31,13 +31,17 @@ - + + - + + - + + + diff --git a/helm/style/html_init.xsl b/helm/style/html_init.xsl index 46fc61b24..91d978f5c 100644 --- a/helm/style/html_init.xsl +++ b/helm/style/html_init.xsl @@ -481,8 +481,6 @@ - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + - + select="document($InductiveTypeUrl)/ConstantType/PROD/decl/*[1]"/> - + @@ -65,7 +126,7 @@ - + + used for rendering (it could be omitted ??) --> + + + + + + + + + + + @@ -179,28 +244,24 @@ If this is not the case, not good rendering looks possible. Check_args returns a boolean. --> + + + - - - - - - - - - - - + + + select="($no_actual_abst_of_arg >= $no_expected_arg_of_arg)"/> @@ -208,25 +269,8 @@ - + - - - - - - - - - - - - - - - - - + - - - - - - - + + + + - + - + - + - - + select="$constructor_args[position()>1]"/> + + - - - + + + - - - - - - - - - - - + - - - - - - - + + + + - + - + + select="$actual_args[2]/*"/> - - - + + + - - - + + + - - - - - - - - - - - - - - - - + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - +
diff --git a/helm/style/ite.xsl b/helm/style/ite.xsl new file mode 100644 index 000000000..1b0e14a72 --- /dev/null +++ b/helm/style/ite.xsl @@ -0,0 +1,48 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ite + + + + + + + + + diff --git a/helm/style/link.xsl b/helm/style/link.xsl index e3568a18f..e6d639a3b 100644 --- a/helm/style/link.xsl +++ b/helm/style/link.xsl @@ -39,6 +39,8 @@ + + @@ -52,7 +54,14 @@ xlink:href) --> - + + + + + + + + diff --git a/helm/style/logic.xsl b/helm/style/logic.xsl new file mode 100644 index 000000000..0a261260a --- /dev/null +++ b/helm/style/logic.xsl @@ -0,0 +1,155 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 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_meta_and_dep_graph.xsl b/helm/style/mk_meta_and_dep_graph.xsl index a9a9a954b..c860e4b46 100644 --- a/helm/style/mk_meta_and_dep_graph.xsl +++ b/helm/style/mk_meta_and_dep_graph.xsl @@ -24,16 +24,10 @@ - - -]> - + xmlns:h="http://www.cs.unibo.it/helm/schemas/mattone.rdf#"> @@ -159,9 +153,9 @@ - strict digraph L0 { size = "83,83"; node [style=filled, shape = box];&CSCbr; + strict digraph L0 { size = "83,83"; node [style=filled, shape = box]; @@ -239,7 +233,7 @@ ,color=red - ];&CSCbr; + ]; @@ -248,12 +242,12 @@ - + - + @@ -263,7 +257,7 @@ -> - ;&CSCbr; + ;
diff --git a/helm/style/mk_meta_theory.xsl b/helm/style/mk_meta_theory.xsl index 3a07962a9..e433c4b26 100644 --- a/helm/style/mk_meta_theory.xsl +++ b/helm/style/mk_meta_theory.xsl @@ -28,25 +28,19 @@ xmlns:xsl="http://www.w3.org/1999/XSL/Transform" xmlns:ht="http://www.cs.unibo.it/helm/namespaces/helm-theory" xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" - xmlns:h="http:/www.cs.unibo.it/helm/schemas/schema-h.rdf#"> - - - - - - + xmlns:h="http://www.cs.unibo.it/helm/schemas/mattone.rdf#"> - Occurrences of <xsl:value-of select="*/*/@rdf:value"/> + Occurrences of <xsl:value-of select="*/*/@rdf:about"/> - + @@ -55,15 +49,15 @@ + select="count(*/h:Occurrence/h:position[text()='MainConclusion'])"/> + select="count(*/h:Occurrence/h:position[text()='InConclusion'])"/> + select="count(*/h:Occurrence/h:position[text()='MainHypothesis'])"/> + select="count(*/h:Occurrence/h:position[text()='InHypothesis'])"/> + select="count(*/h:Occurrence/h:position[text()='InBody'])"/>

Occurrences of

    @@ -92,17 +86,17 @@

    Head position inside conclusion:

    - +
    - +

    Head position inside conclusion:

    - +
    - +
    @@ -111,17 +105,17 @@

    Inside conclusion:

    - +
    - +

    Inside conclusion:

    - +
    - +
    @@ -130,17 +124,17 @@

    Head position inside an hypothesis:

    - +
    - +

    Head position inside an hypothesis:

    - +
    - +
    @@ -149,26 +143,26 @@

    Inside an hypothesis:

    - +
    - +

    Inside an hypothesis:

    - +
    - +

    Inside the body:

    - +
    - +
    diff --git a/helm/style/mmlctop.xsl b/helm/style/mmlctop.xsl index 554c3a87b..b63ebee8a 100644 --- a/helm/style/mmlctop.xsl +++ b/helm/style/mmlctop.xsl @@ -1293,18 +1293,38 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + { + + + := + + + } + + + + + + + + + + + + @ + + + + + + + + + + + + + + + + @ + + + + + + + + + + + + + + if + + + + + + + + then + + + + + + + + else + + + + + + + + + if + + then + + else + + + + + @@ -1478,23 +1568,112 @@ which generates the toplevel element (see for instance xlink) --> - - - - Rewrite - _ - - _ - with - _ - - _ - by - _ - - - - + + + + + + + + + + + + + + + + + Rewrite + _ + + + + + + + + + + with + _ + + + + + + + + by + _ + + + + + + + + + + with + _ + + _ + by + _ + + + + + + + + + + + + Rewrite + _ + + _ + with + _ + + + + + + + + by + _ + + + + + + + + + + Rewrite + _ + + _ + with + _ + + _ + by + _ + + + + + +
    - + @@ -1977,7 +2156,7 @@ which generates the toplevel element (see for instance xlink) --> - ERROR + ERROR("") @@ -2086,6 +2265,24 @@ which generates the toplevel element (see for instance xlink) --> + + + + + + + + + + + + + + + + + + @@ -2113,14 +2310,24 @@ which generates the toplevel element (see for instance xlink) --> - - + + + + + + 3 + + + + + + - - + + - + @@ -2128,7 +2335,7 @@ which generates the toplevel element (see for instance xlink) --> - + diff --git a/helm/style/mmlnotation.xsl b/helm/style/mmlnotation.xsl index 5cf944e72..7081ad83f 100644 --- a/helm/style/mmlnotation.xsl +++ b/helm/style/mmlnotation.xsl @@ -139,26 +139,24 @@ ( - + + + + + + + + __ + + + + + + + - - - - - __ - - - - - - - - - - - @@ -396,4 +394,4 @@ - \ No newline at end of file + diff --git a/helm/style/objcontent.xsl b/helm/style/objcontent.xsl index ceb7a22ba..5b243e783 100644 --- a/helm/style/objcontent.xsl +++ b/helm/style/objcontent.xsl @@ -52,6 +52,51 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -73,11 +118,15 @@ - + + - + + + - + click here - + - - + + - + + + + + + - + - + + - + @@ -133,7 +188,7 @@ - + diff --git a/helm/style/objtheorycontent.xsl b/helm/style/objtheorycontent.xsl index 7d890d611..5bad7e108 100644 --- a/helm/style/objtheorycontent.xsl +++ b/helm/style/objtheorycontent.xsl @@ -43,42 +43,42 @@ - - + + - + - + + + - - - + - + - + - + - + diff --git a/helm/style/params.xsl b/helm/style/params.xsl index d703bfe06..1b5f41670 100644 --- a/helm/style/params.xsl +++ b/helm/style/params.xsl @@ -39,16 +39,18 @@ + - + + @@ -98,6 +100,25 @@ + + + + + + + + + + + + + + + + + @@ -163,14 +184,11 @@ - - - - - - - - + + + + @@ -179,7 +197,9 @@ - 0 + + 0 + @@ -198,11 +218,13 @@ - + - 0 + + 0 + @@ -275,25 +297,59 @@ - - - - - - + + + + + + + + + + + + + + + + + + + + + + + - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - + @@ -356,7 +412,7 @@ - + diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl index f61cbe6d9..dbcfabaa3 100644 --- a/helm/style/proofs.xsl +++ b/helm/style/proofs.xsl @@ -34,15 +34,19 @@ xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:helm="http://www.cs.unibo.it/helm"> + + + + + - - - + + @@ -59,10 +63,10 @@ + proof - @@ -76,8 +80,19 @@ - + + + + + + + + + + + + @@ -87,30 +102,114 @@ - + proof - + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + yes + + + + + + + proof + + let_in + + + + + + + + + + + + + + + + let_in + + + + + + + + + + + + - + proof - @@ -132,588 +231,32 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - eq_chain - - - - - - - - - - - - - diseq_chain - - - - - - - - - - - - - - diseq_chain - - - - - - - - - - - - - - - - - diseq_chain - - - - - - - - - - - - - - diseq_chain - - - - - - - - - - - - - - diseq_chain - - - - - - - - - - - - - - diseq_chain - - - - - - - - - - - - - - - diseq_chain - - - - - - - - - - - - - - - diseq_chain - - - - - - - - - - - - - - - - - - rw_step - - - - - - - - - - - - - - - - rewrite_and_apply - - rw_step - - - - - - - - - - - - - - - - letin - - let - - - - - - - - - - - - - rewrite_and_apply - - rw_step - - - - - - - - - - - - - - - - - - - - - - - letin - - - - - - rewrite_and_apply - - rw_step - - - - - - - - - - - - - - - - - - - - - - - - false_ind - cic:/Coq/Init/Logic/False_ind.con - - - - - - - and_ind - - - - - - - - - - - - - - full_or_ind - - - - - - left_case - - - - - - - - - - - - right_case - - - - - - - - - - - - - - - or_ind - - - - - - - - - - - - - - ex_ind - - - - - - - - - + - + + - letin - - let + let_in + - + - - - + + + @@ -721,32 +264,6 @@ - - - - - rw_step - - - - - - - - - - - - - - @@ -876,6 +393,49 @@ + + + + + + + + + + + + + + + yes + + + + + + + let + + + + + + + + + + + + + + + + + + + + - + @@ -926,7 +487,8 @@ - + @@ -960,7 +522,7 @@ - + @@ -993,27 +555,5 @@ - - diff --git a/helm/style/rewrite.xsl b/helm/style/rewrite.xsl new file mode 100644 index 000000000..e361944d3 --- /dev/null +++ b/helm/style/rewrite.xsl @@ -0,0 +1,135 @@ + + + + + + + + + + + + + + + + + + + + + + + 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/ring.xsl b/helm/style/ring.xsl index d57723ea8..5136e77d5 100644 --- a/helm/style/ring.xsl +++ b/helm/style/ring.xsl @@ -4,12 +4,12 @@ xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:helm="http://www.cs.unibo.it/helm"> - + - + app - + ... @@ -19,12 +19,12 @@ - + - + - - + + @@ -33,16 +33,15 @@ - + - + app - + - - + + @@ -54,28 +53,34 @@ - + + + ERROR INTERP: + + + + + + + - - - + + + 0 - - - + + + 1 - + + @@ -85,8 +90,8 @@ - + + @@ -96,8 +101,8 @@ - + + @@ -107,24 +112,21 @@ - + - + - + diff --git a/helm/style/xslt_index.txt b/helm/style/xslt_index.txt index 2f31b969a..84cd46836 100644 --- a/helm/style/xslt_index.txt +++ b/helm/style/xslt_index.txt @@ -3,6 +3,7 @@ annotatedpres.xsl content.xsl content_to_html.xsl contentlib.xsl +diseq.xsl drop_coercions.xsl expandobj.xsl genmmlid.xsl @@ -12,9 +13,11 @@ 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 @@ -27,6 +30,7 @@ objcontent.xsl objtheorycontent.xsl params.xsl proofs.xsl +rewrite.xsl ricerca.xsl ring.xsl rootcontent.xsl