# HG changeset patch
# User hoelzl
# Date 1428831210 -7200
# Node ID 071a99649dde4f93f97e329b11455d65dd82f567
# Parent  218fcc645d22e9a27b200cb574fd36f718d43547
add quantifier syntax for eventually

diff -r 218fcc645d22 -r 071a99649dde src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Sun Apr 12 11:33:19 2015 +0200
+++ b/src/HOL/Filter.thy	Sun Apr 12 11:33:30 2015 +0200
@@ -39,6 +39,15 @@
 definition eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool"
   where "eventually P F \<longleftrightarrow> Rep_filter F P"
 
+syntax
+  "_eventually"  :: "pttrn => 'a filter => bool => bool"      ("(3ALL _ in _./ _)" [0, 0, 10] 10)
+
+syntax (xsymbols)
+  "_eventually"  :: "pttrn => 'a filter => bool => bool"      ("(3\<forall>_ in _./ _)" [0, 0, 10] 10)
+
+translations
+  "\<forall>x in F. P" == "CONST eventually (%x. P) F"
+
 lemma eventually_Abs_filter:
   assumes "is_filter F" shows "eventually P (Abs_filter F) = F P"
   unfolding eventually_def using assms by (simp add: Abs_filter_inverse)