First version of Di Lena's stylesheet generator (for the HELM DTD).

[helm.git] / helm / meta_style / basic.xml

diff --git a/helm/meta_style/basic.xml b/helm/meta_style/basic.xml
new file mode 100644 (file)
index 0000000..8b4c245
--- /dev/null
+++ b/helm/meta_style/basic.xml
@@ -0,0 +1,77 @@
+<!DOCTYPE OpList SYSTEM "operator.dtd">
+
+
+<OpList xmlns:m="http://www.w3.org/1998/Math/MathML">
+
+<!-- ************************* LOGIC *********************************-->
+
+<Operator
+ name  = "AND"
+ uri   = "cic:/Coq/Init/Logic/Conjunction/and.ind"
+ arity = "2"
+ m-tag = "and"/>
+
+<Operator
+ name  = "OR"
+ uri   = "cic:/Coq/Init/Logic/Disjunction/or.ind"
+ arity = "2"
+ m-tag = "or"/>
+
+<Operator
+ name  = "NOT" 
+ uri   = "cic:/Coq/Init/Logic/not.con"
+ arity = "1"
+ m-tag = "not"/>
+ 
+ 
+<!-- EQUALITY and TYPE EQUALITY -->
+
+<Operator
+ name  = "EQUALITY and TYPE EQUALITY"
+ uri   = "cic:/Coq/Init/Logic/Equality/eq.ind | cic:/Coq/Init/Logic_Type/eqT.ind"
+ hide  = "1"
+ arity = "2"
+ m-tag = "eq"/>
+
+<NotOperator
+ name  = "NOT-EQ and NOT-EQT"
+ uri   = "cic:/Coq/Init/Logic/Equality/eq.ind | cic:/Coq/Init/Logic_Type/eqT.ind"
+ hide  = "1"
+ arity = "2">
+       <mapp>
+               <m:neq/>
+               <param id="1"/>
+               <param id="2" mode="set"/>
+       </mapp>
+</NotOperator>
+
+<Operator
+ name  = "EXIST"
+ uri   = "cic:/Coq/Init/Logic/First_order_quantifiers/ex.ind | cic:/Coq/Init/Logic_Type/exT.ind"
+ arity = "2">
+       <mapp>
+               <mop tag="exist"/>
+               <mbvar name="x"/>
+               <m:condition>
+                       <param id="1" mode="pure"/>
+               </m:condition>
+               <param id="2" bvar="x"/>
+       </mapp>
+</Operator>
+
+<Operator
+ name  = "EXIST"
+ uri   = "cic:/Coq/Init/Logic/First_order_quantifiers/ex2.ind | cic:/Coq/Init/Logic_Type/exT2.ind"
+ hide  = "1"
+ arity = "2">
+       <mapp>
+               <mop tag="exist"/>
+               <mbvar name="x"/>
+               <m:condition>
+                       <param id="1" bvar="x"/>
+               </m:condition>
+               <param id="2" bvar="x"/>
+       </mapp>
+</Operator>
+
+</OpList>