# HG changeset patch
# User berghofe
# Date 1173540357 -3600
# Node ID 1d00d26fee0db986dcebd89f964999d40e596ecd
# Parent  28344ccffc35a121bf7270271c98a9e6752d7705
Renamed INF to INFM to avoid clash with INF operator defined in FixedPoint theory.

diff -r 28344ccffc35 -r 1d00d26fee0d src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Sat Mar 10 16:24:52 2007 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Sat Mar 10 16:25:57 2007 +0100
@@ -358,12 +358,12 @@
 *}
 
 definition
-  Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "INF " 10) where
+  Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "INFM " 10) where
   "Inf_many P = infinite {x. P x}"
 
 definition
   Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "MOST " 10) where
-  "Alm_all P = (\<not> (INF x. \<not> P x))"
+  "Alm_all P = (\<not> (INFM x. \<not> P x))"
 
 notation (xsymbols)
   Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and