# HG changeset patch
# User wenzelm
# Date 1294441331 -3600
# Node ID 8fc17c5e11c096148f8eefae29331c2de72ed05a
# Parent  73981e95b30b53446d84cde8a9f712e934f0745f
tuned headers;

diff -r 73981e95b30b -r 8fc17c5e11c0 src/HOL/Quotient_Examples/FSet.thy
--- a/src/HOL/Quotient_Examples/FSet.thy	Fri Jan 07 23:46:06 2011 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy	Sat Jan 08 00:02:11 2011 +0100
@@ -2,7 +2,7 @@
     Author:     Cezary Kaliszyk, TU Munich
     Author:     Christian Urban, TU Munich
 
-    Type of finite sets.
+Type of finite sets.
 *)
 
 theory FSet
diff -r 73981e95b30b -r 8fc17c5e11c0 src/HOL/Quotient_Examples/Quotient_Int.thy
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Fri Jan 07 23:46:06 2011 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Sat Jan 08 00:02:11 2011 +0100
@@ -2,8 +2,10 @@
     Author:     Cezary Kaliszyk
     Author:     Christian Urban
 
-Integers based on Quotients, based on an older version by Larry Paulson.
+Integers based on Quotients, based on an older version by Larry
+Paulson.
 *)
+
 theory Quotient_Int
 imports "~~/src/HOL/Library/Quotient_Product" Nat
 begin
diff -r 73981e95b30b -r 8fc17c5e11c0 src/HOL/Quotient_Examples/Quotient_Message.thy
--- a/src/HOL/Quotient_Examples/Quotient_Message.thy	Fri Jan 07 23:46:06 2011 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Message.thy	Sat Jan 08 00:02:11 2011 +0100
@@ -3,6 +3,7 @@
 
 Message datatype, based on an older version by Larry Paulson.
 *)
+
 theory Quotient_Message
 imports Main Quotient_Syntax
 begin
diff -r 73981e95b30b -r 8fc17c5e11c0 src/HOL/Tools/list_to_set_comprehension.ML
--- a/src/HOL/Tools/list_to_set_comprehension.ML	Fri Jan 07 23:46:06 2011 +0100
+++ b/src/HOL/Tools/list_to_set_comprehension.ML	Sat Jan 08 00:02:11 2011 +0100
@@ -1,7 +1,8 @@
-(*  Title:  HOL/Tools/list_to_set_comprehension.ML
-    Author: Lukas Bulwahn, TU Muenchen
+(*  Title:      HOL/Tools/list_to_set_comprehension.ML
+    Author:     Lukas Bulwahn, TU Muenchen
 
-  Simproc for rewriting list comprehensions applied to List.set to set comprehension
+Simproc for rewriting list comprehensions applied to List.set to set
+comprehension.
 *)
 
 signature LIST_TO_SET_COMPREHENSION =