src/HOL/Tools/Quotient/quotient_info.ML
changeset 38764 e6a18808873c
parent 38759 37a9092de102
child 40236 8694a12611f9
     1.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Thu Aug 26 20:42:09 2010 +0200
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Thu Aug 26 21:04:22 2010 +0200
     1.3 @@ -235,39 +235,49 @@
     1.4  
     1.5  (* equivalence relation theorems *)
     1.6  structure EquivRules = Named_Thms
     1.7 -  (val name = "quot_equiv"
     1.8 -   val description = "Equivalence relation theorems.")
     1.9 +(
    1.10 +  val name = "quot_equiv"
    1.11 +  val description = "equivalence relation theorems"
    1.12 +)
    1.13  
    1.14  val equiv_rules_get = EquivRules.get
    1.15  val equiv_rules_add = EquivRules.add
    1.16  
    1.17  (* respectfulness theorems *)
    1.18  structure RspRules = Named_Thms
    1.19 -  (val name = "quot_respect"
    1.20 -   val description = "Respectfulness theorems.")
    1.21 +(
    1.22 +  val name = "quot_respect"
    1.23 +  val description = "respectfulness theorems"
    1.24 +)
    1.25  
    1.26  val rsp_rules_get = RspRules.get
    1.27  val rsp_rules_add = RspRules.add
    1.28  
    1.29  (* preservation theorems *)
    1.30  structure PrsRules = Named_Thms
    1.31 -  (val name = "quot_preserve"
    1.32 -   val description = "Preservation theorems.")
    1.33 +(
    1.34 +  val name = "quot_preserve"
    1.35 +  val description = "preservation theorems"
    1.36 +)
    1.37  
    1.38  val prs_rules_get = PrsRules.get
    1.39  val prs_rules_add = PrsRules.add
    1.40  
    1.41  (* id simplification theorems *)
    1.42  structure IdSimps = Named_Thms
    1.43 -  (val name = "id_simps"
    1.44 -   val description = "Identity simp rules for maps.")
    1.45 +(
    1.46 +  val name = "id_simps"
    1.47 +  val description = "identity simp rules for maps"
    1.48 +)
    1.49  
    1.50  val id_simps_get = IdSimps.get
    1.51  
    1.52  (* quotient theorems *)
    1.53  structure QuotientRules = Named_Thms
    1.54 -  (val name = "quot_thm"
    1.55 -   val description = "Quotient theorems.")
    1.56 +(
    1.57 +  val name = "quot_thm"
    1.58 +  val description = "quotient theorems"
    1.59 +)
    1.60  
    1.61  val quotient_rules_get = QuotientRules.get
    1.62  val quotient_rules_add = QuotientRules.add