src/HOL/Wellfounded_Relations.thy
changeset 11008 f7333f055ef6
parent 10213 01c2744a3786
child 11136 e34e7f6d9b57
     1.1 --- a/src/HOL/Wellfounded_Relations.thy	Wed Jan 31 10:15:01 2001 +0100
     1.2 +++ b/src/HOL/Wellfounded_Relations.thy	Wed Jan 31 10:15:55 2001 +0100
     1.3 @@ -36,7 +36,7 @@
     1.4  "finite_psubset == {(A,B). A < B & finite B}"
     1.5  
     1.6  (* For rec_defs where the first n parameters stay unchanged in the recursive
     1.7 -   call. See While for an application.
     1.8 +   call. See Library/While_Combinator.thy for an application.
     1.9  *)
    1.10   same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
    1.11  "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"