# HG changeset patch
# User wenzelm
# Date 939140794 -7200
# Node ID 01386eb4eab02084c8e2a4fddd59db3d7ac88741
# Parent  874abb8aa65b5cf23ca1e4132e77723c868d7b46
fixed title;

diff -r 874abb8aa65b -r 01386eb4eab0 src/HOL/ex/Points.thy
--- 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. *};