tuned comment
authorkuncar
Mon Mar 26 18:32:22 2012 +0200 (2012-03-26)
changeset 4711981ada90d8220
parent 47118 2fe7a42ece1d
child 47120 500a5d97511a
child 47124 960f0a4404c7
tuned comment
src/HOL/Quotient_Examples/Lift_Fun.thy
     1.1 --- a/src/HOL/Quotient_Examples/Lift_Fun.thy	Mon Mar 26 17:58:47 2012 +0200
     1.2 +++ b/src/HOL/Quotient_Examples/Lift_Fun.thy	Mon Mar 26 18:32:22 2012 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  imports Main "~~/src/HOL/Library/Quotient_Syntax"
     1.5  begin
     1.6  
     1.7 -text {* This file is meant as a test case for features introduced in the changeset 2d8949268303. 
     1.8 +text {* This file is meant as a test case. 
     1.9    It contains examples of lifting definitions with quotients that have contravariant 
    1.10    type variables or type variables which are covariant and contravariant in the same time. *}
    1.11