src/HOL/UNITY/ELT.thy

--- a/src/HOL/UNITY/ELT.thy	Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/ELT.thy	Fri Jan 14 12:17:53 2000 +0100
@@ -43,6 +43,10 @@
 
 
 constdefs
+  
+  (*the set of all sets determined by f alone*)
+  givenBy :: "['a => 'b] => 'a set set"
+    "givenBy f == range (%B. f-`` B)"
 
   (*visible version of the LEADS-TO relation*)
   leadsETo :: "['a set, 'a set set, 'a set] => 'a program set"