No longer in use. The official repository for the

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

diff --git a/helm/meta_style/list.xml b/helm/meta_style/list.xml
deleted file mode 100644 (file)
index 9ed07d6..0000000
--- a/helm/meta_style/list.xml
+++ /dev/null
@@ -1,60 +0,0 @@
-<!DOCTYPE OpList SYSTEM "operator.dtd">
-
-<!-- ************************** LISTS ****************************** -->
-
-<OpList xmlns:m="http://www.w3.org/1998/Math/MathML">
-
-<!-- CSC: manca
-<Operator
- name  = "CONS"
- uri   = "cic:/Coq/Lists/PolyList/list.ind"
- arity = "2"
- m-tag = "???"/>
-
-<Operator
- name  = "NIL"
- uri   = "cic:/Coq/Lists/PolyList/list.ind"
- arity = "0"
- m-tag = "???"/> -->
-
-<Operator
- name  = "APPEND"
- uri   = "cic:/Coq/Lists/PolyList/app.con"
- cook  = "true"
- arity = "2">
-       <mapp>
-               <m:csymbol>append</m:csymbol>
-               <param id="1"/>
-               <param id="2"/>
-       </mapp>
-</Operator>
-
-<Operator
- name  = "IN"
- uri   = "cic:/Coq/Lists/PolyList/In.con | cic:/Coq/Lists/TheoryList/In_spec.ind | cic:/Coq/Lists/ListSet/set_In.con | cic:/Coq/Lists/ListSet/set_mem.con"
- cook  = "true"
- arity = "2"
- m-tag = "in"/>
-
-<Operator
- name  = "INCL"
- uri   = "cic:/Coq/Lists/PolyList/incl.con"
- cook  = "true"
- arity = "2"
- m-tag = "subset"/>
-
-<Operator
- name  = "INTER"
- uri   = "cic:/Coq/Lists/ListSet/set_inter.con"
- cook  = "true"
- arity = "2"
- m-tag = "intersect"/>
-
-<Operator
- name  = "LENGTH"
- uri   = "cic:/Coq/Lists/PolyList/length.con"
- cook  = "true"
- arity = "1"
- m-tag = "card"/>
-
-</OpList>