# HG changeset patch
# User nipkow
# Date 921771754 -3600
# Node ID 2b23e14dd386fec1e5c7a140edd3449b8c5ef525
# Parent  2462d0c077b52fee56e1a2e0734999f9531e3274
New bounded quantifier syntax: !x<i. P etc

diff -r 2462d0c077b5 -r 2b23e14dd386 src/HOL/Ord.thy
--- a/src/HOL/Ord.thy	Thu Mar 18 11:19:03 1999 +0100
+++ b/src/HOL/Ord.thy	Thu Mar 18 16:42:34 1999 +0100
@@ -55,4 +55,16 @@
 axclass linorder < order
   linorder_linear "x <= y | y <= x"
 
+(*bounded quantifiers*)
+syntax
+  "@lessAll" :: [idt, 'a, bool] => bool   ("(3! _<_./ _)"  [0, 0, 10] 10)
+  "@lessEx"  :: [idt, 'a, bool] => bool   ("(3? _<_./ _)"  [0, 0, 10] 10)
+  "@leAll"   :: [idt, 'a, bool] => bool   ("(3! _<=_./ _)" [0, 0, 10] 10)
+  "@leEx"    :: [idt, 'a, bool] => bool   ("(3? _<=_./ _)" [0, 0, 10] 10)
+translations
+ "! x<y.  P"  =>  "! x. x < y  --> P"
+ "! x<=y. P"  =>  "! x. x <= y --> P"
+ "? x<y.  P"  =>  "? x. x < y  & P"
+ "? x<=y. P"  =>  "! x. x <= y & P"
+
 end