--- 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*)