src/HOL/Wellfounded.thy
changeset 28524 644b62cf678f
parent 28260 703046c93ffe
child 28562 4e74209f113e
     1.1 --- a/src/HOL/Wellfounded.thy	Tue Oct 07 16:07:40 2008 +0200
     1.2 +++ b/src/HOL/Wellfounded.thy	Tue Oct 07 16:07:50 2008 +0200
     1.3 @@ -33,7 +33,7 @@
     1.4    "acyclic r == !x. (x,x) ~: r^+"
     1.5  
     1.6    cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
     1.7 -  "cut f r x == (%y. if (y,x):r then f y else arbitrary)"
     1.8 +  "cut f r x == (%y. if (y,x):r then f y else undefined)"
     1.9  
    1.10    adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool"
    1.11    "adm_wf R F == ALL f g x.