author | wenzelm |
Tue, 05 Oct 1999 18:26:34 +0200 | |
changeset 7742 | 01386eb4eab0 |
parent 7741 | 874abb8aa65b |
child 7743 | 64662aa3c173 |
--- a/src/HOL/ex/Points.thy Tue Oct 05 18:16:53 1999 +0200 +++ b/src/HOL/ex/Points.thy Tue Oct 05 18:26:34 1999 +0200 @@ -5,7 +5,7 @@ theory Points = Main:; -title {* Basic use of extensible records in HOL, including the famous points +text {* Basic use of extensible records in HOL, including the famous points and coloured points. *};