improved theory reference in comment
authoroheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008f7333f055ef6
parent 11007 438f31613093
child 11009 9e0ad9a5f9bb
improved theory reference in comment
src/HOL/Wellfounded_Relations.thy
     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}"