X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmeta_style%2Fbasic.xml;fp=helm%2Fmeta_style%2Fbasic.xml;h=8b4c24520076e0c2454c91f2513b519cd3cf3a90;hb=a2dcdb25b6efbd2623913ecf8f0f7ad3fb60bc75;hp=0000000000000000000000000000000000000000;hpb=5216557e4adc44b1f53eac3377d9c63b0ecad478;p=helm.git

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 @@
+<!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>