# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269697102 -3600
# Node ID ae54ce4cde545394be8ebbaa13e6811a59ec3f6c
# Parent  b8a07a3c16925d57ada8ff1a4e5289603ba4af32
Remove list_eq notation.

diff -r b8a07a3c1692 -r ae54ce4cde54 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Sat Mar 27 13:50:59 2010 +0100
+++ b/Nominal/FSet.thy	Sat Mar 27 14:38:22 2010 +0100
@@ -424,4 +424,7 @@
   | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
 *}
 
+no_notation
+  list_eq (infix "\<approx>" 50)
+
 end
diff -r b8a07a3c1692 -r ae54ce4cde54 Nominal/Nominal2_FSet.thy
--- a/Nominal/Nominal2_FSet.thy	Sat Mar 27 13:50:59 2010 +0100
+++ b/Nominal/Nominal2_FSet.thy	Sat Mar 27 14:38:22 2010 +0100
@@ -3,7 +3,7 @@
 begin
 
 lemma permute_rsp_fset[quot_respect]:
-  "(op = ===> op \<approx> ===> op \<approx>) permute permute"
+  "(op = ===> list_eq ===> list_eq) permute permute"
   apply (simp add: eqvts[symmetric])
   apply clarify
   apply (subst permute_minus_cancel(1)[symmetric, of "xb"])