# HG changeset patch
# User haftmann
# Date 1158672108 -7200
# Node ID 7cbb224598b25ab009d55df6cf4ad881128760d9
# Parent  bf92900995f8b0ee88d422226a46ed54fe6ef8e0
text cleanup

diff -r bf92900995f8 -r 7cbb224598b2 src/HOL/PreList.thy
--- a/src/HOL/PreList.thy	Tue Sep 19 15:21:44 2006 +0200
+++ b/src/HOL/PreList.thy	Tue Sep 19 15:21:48 2006 +0200
@@ -4,14 +4,15 @@
     Copyright   2000 TU Muenchen
 *)
 
-header{*A Basis for Building the Theory of Lists*}
+header {* A Basis for Building the Theory of Lists *}
 
 theory PreList
 imports Wellfounded_Relations Presburger Relation_Power Binomial
 begin
 
 text {*
-  Is defined separately to serve as a basis for theory ToyList in the
-  documentation. *}
+  This is defined separately to serve as a basis for
+  theory ToyList in the documentation.
+*}
 
 end