# HG changeset patch
# User wenzelm
# Date 968095214 -7200
# Node ID 193dc80eaee9ba26840f5e58d2cab1fceeaf1a37
# Parent  2092298f74218d9b1b185b98020dd40fb60e1c7a
tuned comment;

diff -r 2092298f7421 -r 193dc80eaee9 src/HOL/WF_Rel.thy
--- a/src/HOL/WF_Rel.thy	Mon Sep 04 21:19:27 2000 +0200
+++ b/src/HOL/WF_Rel.thy	Mon Sep 04 21:20:14 2000 +0200
@@ -12,7 +12,7 @@
 
 WF_Rel = Finite +
 
-(* actually belongs to Finite.thy *)
+(* actually belongs to theory Finite *)
 instance unit :: finite                  (finite_unit)
 instance "*" :: (finite,finite) finite   (finite_Prod)