tuned headers;
authorwenzelm
Sat Jan 08 00:02:11 2011 +0100 (2011-01-08)
changeset 414678fc17c5e11c0
parent 41466 73981e95b30b
child 41468 0e4f6cf20cdf
tuned headers;
src/HOL/Quotient_Examples/FSet.thy
src/HOL/Quotient_Examples/Quotient_Int.thy
src/HOL/Quotient_Examples/Quotient_Message.thy
src/HOL/Tools/list_to_set_comprehension.ML
     1.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Fri Jan 07 23:46:06 2011 +0100
     1.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Sat Jan 08 00:02:11 2011 +0100
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Cezary Kaliszyk, TU Munich
     1.5      Author:     Christian Urban, TU Munich
     1.6  
     1.7 -    Type of finite sets.
     1.8 +Type of finite sets.
     1.9  *)
    1.10  
    1.11  theory FSet
     2.1 --- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Fri Jan 07 23:46:06 2011 +0100
     2.2 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Sat Jan 08 00:02:11 2011 +0100
     2.3 @@ -2,8 +2,10 @@
     2.4      Author:     Cezary Kaliszyk
     2.5      Author:     Christian Urban
     2.6  
     2.7 -Integers based on Quotients, based on an older version by Larry Paulson.
     2.8 +Integers based on Quotients, based on an older version by Larry
     2.9 +Paulson.
    2.10  *)
    2.11 +
    2.12  theory Quotient_Int
    2.13  imports "~~/src/HOL/Library/Quotient_Product" Nat
    2.14  begin
     3.1 --- a/src/HOL/Quotient_Examples/Quotient_Message.thy	Fri Jan 07 23:46:06 2011 +0100
     3.2 +++ b/src/HOL/Quotient_Examples/Quotient_Message.thy	Sat Jan 08 00:02:11 2011 +0100
     3.3 @@ -3,6 +3,7 @@
     3.4  
     3.5  Message datatype, based on an older version by Larry Paulson.
     3.6  *)
     3.7 +
     3.8  theory Quotient_Message
     3.9  imports Main Quotient_Syntax
    3.10  begin
     4.1 --- a/src/HOL/Tools/list_to_set_comprehension.ML	Fri Jan 07 23:46:06 2011 +0100
     4.2 +++ b/src/HOL/Tools/list_to_set_comprehension.ML	Sat Jan 08 00:02:11 2011 +0100
     4.3 @@ -1,7 +1,8 @@
     4.4 -(*  Title:  HOL/Tools/list_to_set_comprehension.ML
     4.5 -    Author: Lukas Bulwahn, TU Muenchen
     4.6 +(*  Title:      HOL/Tools/list_to_set_comprehension.ML
     4.7 +    Author:     Lukas Bulwahn, TU Muenchen
     4.8  
     4.9 -  Simproc for rewriting list comprehensions applied to List.set to set comprehension
    4.10 +Simproc for rewriting list comprehensions applied to List.set to set
    4.11 +comprehension.
    4.12  *)
    4.13  
    4.14  signature LIST_TO_SET_COMPREHENSION =