src/HOL/Set.thy
changeset 19323 ec5cd5b1804c
parent 19295 c5d236fe9668
child 19363 667b5ea637dd
     1.1 --- a/src/HOL/Set.thy	Thu Mar 23 18:14:06 2006 +0100
     1.2 +++ b/src/HOL/Set.thy	Thu Mar 23 20:03:53 2006 +0100
     1.3 @@ -47,9 +47,11 @@
     1.4  
     1.5  subsection {* Additional concrete syntax *}
     1.6  
     1.7 +abbreviation (output)
     1.8 +  range :: "('a => 'b) => 'b set"             -- "of function"
     1.9 +  "range f  =  f ` UNIV"
    1.10 +
    1.11  syntax
    1.12 -  range         :: "('a => 'b) => 'b set"             -- "of function"
    1.13 -
    1.14    "op ~:"       :: "'a => 'a set => bool"                 ("op ~:")  -- "non-membership"
    1.15    "op ~:"       :: "'a => 'a set => bool"                 ("(_/ ~: _)" [50, 51] 50)
    1.16  
    1.17 @@ -72,7 +74,6 @@
    1.18    "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3? _:_./ _)" [0, 0, 10] 10)
    1.19  
    1.20  translations
    1.21 -  "range f"     == "f`UNIV"
    1.22    "x ~: y"      == "~ (x : y)"
    1.23    "{x, xs}"     == "insert x {xs}"
    1.24    "{x}"         == "insert x {}"