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