--- 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
--- 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
--- 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
--- 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 =