diff -r 63fed88fe8e6 -r e5eb247ad13c src/HOL/Univ.thy
--- a/src/HOL/Univ.thy	Mon Mar 04 12:28:48 1996 +0100
+++ b/src/HOL/Univ.thy	Mon Mar 04 14:37:33 1996 +0100
@@ -22,8 +22,6 @@
   'a item = 'a node set
 
 consts
-  Least     :: (nat=>bool) => nat    (binder "LEAST " 10)
-
   apfst     :: "['a=>'c, 'a*'b] => 'c*'b"
   Push      :: [nat, nat=>nat] => (nat=>nat)
 
@@ -52,9 +50,6 @@
 
 defs
 
-  (*least number operator*)
-  Least_def      "Least(P) == @k. P(k) & (ALL j. j<k --> ~P(j))"
-
   Push_Node_def  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
 
   (*crude "lists" of nats -- needed for the constructions*)