From 1fe35897717252a6d1f65a883900bbe56d946dba Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 6 Dec 2002 17:57:34 +0000
Subject: [PATCH] New notation for ListSet. It often raises ambiguity problems
 in theorems that also use the same notation for PolyLists.

---
 helm/meta_style/list.xml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/helm/meta_style/list.xml b/helm/meta_style/list.xml
index 6e42d21a1..4171058da 100644
--- a/helm/meta_style/list.xml
+++ b/helm/meta_style/list.xml
@@ -33,7 +33,7 @@
 
 <Operator
  name  = "IN"
- uri   = "cic:/Coq/Lists/PolyList/In.con | cic:/Coq/Lists/TheoryList/In_spec.ind"
+ 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"/>
@@ -45,6 +45,13 @@
  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"
-- 
2.39.2