Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
New bounded quantifier syntax: !x<i. P etc
authornipkow
Thu, 18 Mar 1999 16:42:34 +0100
changeset 6402 2b23e14dd386
parent 6401 2462d0c077b5
child 6403 86e9d24f4238
New bounded quantifier syntax: !x<i. P etc
src/HOL/Ord.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle