src/HOL/Univ.thy
changeset 1531 e5eb247ad13c
parent 1475 7f5a4cd08209
child 1562 e98c7f6165c9
     1.1 --- a/src/HOL/Univ.thy	Mon Mar 04 12:28:48 1996 +0100
     1.2 +++ b/src/HOL/Univ.thy	Mon Mar 04 14:37:33 1996 +0100
     1.3 @@ -22,8 +22,6 @@
     1.4    'a item = 'a node set
     1.5  
     1.6  consts
     1.7 -  Least     :: (nat=>bool) => nat    (binder "LEAST " 10)
     1.8 -
     1.9    apfst     :: "['a=>'c, 'a*'b] => 'c*'b"
    1.10    Push      :: [nat, nat=>nat] => (nat=>nat)
    1.11  
    1.12 @@ -52,9 +50,6 @@
    1.13  
    1.14  defs
    1.15  
    1.16 -  (*least number operator*)
    1.17 -  Least_def      "Least(P) == @k. P(k) & (ALL j. j<k --> ~P(j))"
    1.18 -
    1.19    Push_Node_def  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
    1.20  
    1.21    (*crude "lists" of nats -- needed for the constructions*)