| changeset 7742 | 01386eb4eab0 |
| parent 7480 | 0a0e0dbe1269 |
| child 9059 | 2b537d9e6f49 |
--- 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. *};