# HG changeset patch
# User wenzelm
# Date 970528492 -7200
# Node ID 546686f0a6fbab99999946174a1c34e78db3fcbe
# Parent  5a2e00bf1e420feb2bc743b8989e7dd72b7219fa
range declared as syntax;

diff -r 5a2e00bf1e42 -r 546686f0a6fb src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Oct 02 15:13:32 2000 +0200
+++ b/src/HOL/Set.thy	Tue Oct 03 01:14:52 2000 +0200
@@ -33,7 +33,6 @@
   UNION, INTER  :: ['a set, 'a => 'b set] => 'b set     (*general*)
   Union, Inter  :: (('a set) set) => 'a set             (*of a set*)
   Pow           :: 'a set => 'a set set                 (*powerset*)
-  range         :: ('a => 'b) => 'b set                 (*of function*)
   Ball, Bex     :: ['a set, 'a => bool] => bool         (*bounded quantifiers*)
   "image"       :: ['a => 'b, 'a set] => ('b set)   (infixr "``" 90)
   (*membership*)
@@ -43,6 +42,7 @@
 (** Additional concrete syntax **)
 
 syntax
+  range         :: ('a => 'b) => 'b set                 (*of function*)
 
   (* Infix syntax for non-membership *)