# HG changeset patch
# User kuncar
# Date 1332779542 -7200
# Node ID 81ada90d8220e6aa6b684160e44030f0a5a5a377
# Parent  2fe7a42ece1dc4ed718b6d869c516cc2d70ef630
tuned comment

diff -r 2fe7a42ece1d -r 81ada90d8220 src/HOL/Quotient_Examples/Lift_Fun.thy
--- a/src/HOL/Quotient_Examples/Lift_Fun.thy	Mon Mar 26 17:58:47 2012 +0200
+++ b/src/HOL/Quotient_Examples/Lift_Fun.thy	Mon Mar 26 18:32:22 2012 +0200
@@ -9,7 +9,7 @@
 imports Main "~~/src/HOL/Library/Quotient_Syntax"
 begin
 
-text {* This file is meant as a test case for features introduced in the changeset 2d8949268303. 
+text {* This file is meant as a test case. 
   It contains examples of lifting definitions with quotients that have contravariant 
   type variables or type variables which are covariant and contravariant in the same time. *}