]> matita.cs.unibo.it Git - helm.git/blob - helm/meta_style/basic.xml
removed an ancient debugging message
[helm.git] / helm / meta_style / basic.xml
1 <!DOCTYPE OpList SYSTEM "operator.dtd">
2
3
4 <OpList xmlns:m="http://www.w3.org/1998/Math/MathML">
5
6 <!-- ************************* LOGIC *********************************-->
7
8 <Operator
9  name  = "AND"
10  uri   = "cic:/Coq/Init/Logic/Conjunction/and.ind"
11  arity = "2"
12  m-tag = "and"/>
13
14 <Operator
15  name  = "OR"
16  uri   = "cic:/Coq/Init/Logic/Disjunction/or.ind"
17  arity = "2"
18  m-tag = "or"/>
19
20 <Operator
21  name  = "NOT" 
22  uri   = "cic:/Coq/Init/Logic/not.con"
23  arity = "1"
24  m-tag = "not"/>
25  
26  
27 <!-- EQUALITY and TYPE EQUALITY -->
28
29 <Operator
30  name  = "EQUALITY and TYPE EQUALITY"
31  uri   = "cic:/Coq/Init/Logic/Equality/eq.ind | cic:/Coq/Init/Logic_Type/eqT.ind"
32  hide  = "1"
33  arity = "2"
34  m-tag = "eq"/>
35
36 <NotOperator
37  name  = "NOT-EQ and NOT-EQT"
38  uri   = "cic:/Coq/Init/Logic/Equality/eq.ind | cic:/Coq/Init/Logic_Type/eqT.ind"
39  hide  = "1"
40  arity = "2">
41         <mapp>
42                 <m:neq/>
43                 <param id="1"/>
44                 <param id="2" mode="set"/>
45         </mapp>
46 </NotOperator>
47
48 <Operator
49  name  = "EXIST"
50  uri   = "cic:/Coq/Init/Logic/First_order_quantifiers/ex.ind | cic:/Coq/Init/Logic_Type/exT.ind"
51  arity = "2">
52         <mapp>
53                 <mop tag="exists"/>
54                 <mbvar name="x"/>
55                 <m:condition>
56                         <param id="1" mode="pure"/>
57                 </m:condition>
58                 <param id="2" bvar="x"/>
59         </mapp>
60 </Operator>
61
62 <Operator
63  name  = "EXIST"
64  uri   = "cic:/Coq/Init/Logic/First_order_quantifiers/ex2.ind | cic:/Coq/Init/Logic_Type/exT2.ind"
65  hide  = "1"
66  arity = "2">
67         <mapp>
68                 <mop tag="exists"/>
69                 <mbvar name="x"/>
70                 <m:condition>
71                         <param id="1" bvar="x"/>
72                 </m:condition>
73                 <param id="2" bvar="x"/>
74         </mapp>
75 </Operator>
76
77 </OpList>