Mercurial Mercurial > wneuper > isa / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | bz2 | gz | help
_gt, _gt: syntax instead of consts;
authorwenzelm
Sat, 23 Apr 2005 19:49:16 +0200
changeset 15822916b9df2ce9f
parent 15821 ac7ea72c463b
child 15823 d1001770af17
_gt, _gt: syntax instead of consts;
src/HOL/Orderings.thy file | annotate | diff | comparison | revisions 
     1.1 --- a/src/HOL/Orderings.thy	Sat Apr 23 19:49:08 2005 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Sat Apr 23 19:49:16 2005 +0200
     1.3 @@ -39,7 +39,7 @@
     1.4  
     1.5  text{* Syntactic sugar: *}
     1.6  
     1.7 -consts
     1.8 +syntax
     1.9    "_gt" :: "'a::ord => 'a => bool"             (infixl ">" 50)
    1.10    "_ge" :: "'a::ord => 'a => bool"             (infixl ">=" 50)
    1.11  translations
wneuper/isa