From: Irene Schena Date: Wed, 29 Nov 2000 10:45:51 +0000 (+0000) Subject: Modified Files: X-Git-Tag: nogzip~134 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=039f58232964e627868ec21f7c1e64c843204c75;p=helm.git Modified Files: 1) basic.xsl: added to ci elements call-template to insert_subscript 2) content.xsl: modified comments and added to ci elements call-template to insert_subscript 3) mmlextension.xsl: changed EmptySet in emptyset and framewidth=30 in 35. The emptyset marked mi instead of mo 4) mml2mmlv_1_0.xsl: modified comments and added xlink pointer to msqrt 5) objcontent.xsl: added to ci elements call-template to insert_subscript 6) params.xsl: added function insert_subscript 7) proofs.xsl: added to ci elements call-template to insert_subscript 8) reals.xsl: added to ci elements call-template to insert_subscript 9) set.xsl: added to ci elements call-template to insert_subscript --- diff --git a/helm/style/basic.xsl b/helm/style/basic.xsl index a05a281b9..148912aa1 100644 --- a/helm/style/basic.xsl +++ b/helm/style/basic.xsl @@ -66,7 +66,7 @@ - + @@ -91,7 +91,7 @@ - + @@ -105,7 +105,7 @@ app - + @@ -115,13 +115,13 @@ - + app - + diff --git a/helm/style/content.xsl b/helm/style/content.xsl index 68a418dcd..486c0a43f 100644 --- a/helm/style/content.xsl +++ b/helm/style/content.xsl @@ -45,7 +45,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../] - + @@ -66,7 +66,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../] prod - + @@ -87,7 +87,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../] - + @@ -111,7 +111,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../] let - + @@ -142,7 +142,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../] - + @@ -167,21 +167,21 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../] - + - + - + - + @@ -189,7 +189,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../] - + @@ -197,7 +197,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../] - + @@ -215,14 +215,14 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../] - + app - + LAMBDA @@ -237,7 +237,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../] fix - + @@ -246,7 +246,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../] cofix - + @@ -255,7 +255,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../] - + @@ -263,10 +263,15 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../] - + + + + + + diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl index cd6609aa1..0a11b4991 100644 --- a/helm/style/mmlextension.xsl +++ b/helm/style/mmlextension.xsl @@ -18,7 +18,7 @@ - + @@ -878,7 +878,7 @@ _ _ - and apply + and apply to _ @@ -1221,9 +1221,9 @@ - + - + diff --git a/helm/style/objcontent.xsl b/helm/style/objcontent.xsl index 6ad0a4922..112e73ab1 100644 --- a/helm/style/objcontent.xsl +++ b/helm/style/objcontent.xsl @@ -147,7 +147,7 @@ - + @@ -202,7 +202,7 @@ - $ + $ diff --git a/helm/style/params.xsl b/helm/style/params.xsl index 034eeba97..dc59df167 100644 --- a/helm/style/params.xsl +++ b/helm/style/params.xsl @@ -182,6 +182,58 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl index da751e437..cd7593052 100644 --- a/helm/style/proofs.xsl +++ b/helm/style/proofs.xsl @@ -52,9 +52,9 @@ and_ind - + - + @@ -105,7 +105,7 @@ - prev + previous @@ -182,12 +182,12 @@ - + - + @@ -200,7 +200,7 @@ - + diff --git a/helm/style/reals.xsl b/helm/style/reals.xsl index 208d8416e..ff69f9a22 100644 --- a/helm/style/reals.xsl +++ b/helm/style/reals.xsl @@ -192,7 +192,7 @@ - + @@ -246,7 +246,7 @@ - + diff --git a/helm/style/set.xsl b/helm/style/set.xsl index cdb96ec3e..916a92c51 100644 --- a/helm/style/set.xsl +++ b/helm/style/set.xsl @@ -26,7 +26,7 @@ - +