# HG changeset patch
# User oheimb
# Date 980932555 -3600
# Node ID f7333f055ef6975a203536358be8c69f2814ca1e
# Parent  438f316130934b650d43bc05cad57f3f5b774c0c
improved theory reference in comment

diff -r 438f31613093 -r f7333f055ef6 src/HOL/Wellfounded_Relations.thy
--- a/src/HOL/Wellfounded_Relations.thy	Wed Jan 31 10:15:01 2001 +0100
+++ b/src/HOL/Wellfounded_Relations.thy	Wed Jan 31 10:15:55 2001 +0100
@@ -36,7 +36,7 @@
 "finite_psubset == {(A,B). A < B & finite B}"
 
 (* For rec_defs where the first n parameters stay unchanged in the recursive
-   call. See While for an application.
+   call. See Library/While_Combinator.thy for an application.
 *)
  same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
 "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"