Quot/quotient_info.ML
changeset 636 520a4084d064
parent 614 51a4208162ed
child 643 cd4226736c37
equal deleted inserted replaced
633:2e51e1315839 636:520a4084d064
    24   val print_qconstinfo: Proof.context -> unit
    24   val print_qconstinfo: Proof.context -> unit
    25 
    25 
    26   val equiv_rules_get: Proof.context -> thm list
    26   val equiv_rules_get: Proof.context -> thm list
    27   val equiv_rules_add: attribute
    27   val equiv_rules_add: attribute
    28   val rsp_rules_get: Proof.context -> thm list  
    28   val rsp_rules_get: Proof.context -> thm list  
       
    29   val prs_rules_get: Proof.context -> thm list  
    29   val id_simps_get: Proof.context -> thm list
    30   val id_simps_get: Proof.context -> thm list
    30   val quotient_rules_get: Proof.context -> thm list
    31   val quotient_rules_get: Proof.context -> thm list
    31   val quotient_rules_add: attribute
    32   val quotient_rules_add: attribute
    32 end;
    33 end;
    33 
    34 
   178 (* FIXME/TODO: check the various lemmas conform *)
   179 (* FIXME/TODO: check the various lemmas conform *)
   179 (* with the required shape                      *)
   180 (* with the required shape                      *)
   180 
   181 
   181 (* equivalence relation theorems *)
   182 (* equivalence relation theorems *)
   182 structure EquivRules = Named_Thms
   183 structure EquivRules = Named_Thms
   183   (val name = "quotient_equiv"
   184   (val name = "quot_equiv"
   184    val description = "Equivalence relation theorems.")
   185    val description = "Equivalence relation theorems.")
   185 
   186 
   186 val equiv_rules_get = EquivRules.get
   187 val equiv_rules_get = EquivRules.get
   187 val equiv_rules_add = EquivRules.add
   188 val equiv_rules_add = EquivRules.add
   188 
   189 
   189 (* respectfulness theorems *)
   190 (* respectfulness theorems *)
   190 structure RspRules = Named_Thms
   191 structure RspRules = Named_Thms
   191   (val name = "quotient_rsp"
   192   (val name = "quot_respect"
   192    val description = "Respectfulness theorems.")
   193    val description = "Respectfulness theorems.")
   193 
   194 
   194 val rsp_rules_get = RspRules.get
   195 val rsp_rules_get = RspRules.get
       
   196 
       
   197 (* preservation theorems *)
       
   198 structure PrsRules = Named_Thms
       
   199   (val name = "quot_preserve"
       
   200    val description = "Respectfulness theorems.")
       
   201 
       
   202 val prs_rules_get = PrsRules.get
   195 
   203 
   196 (* respectfulness theorems *)
   204 (* respectfulness theorems *)
   197 structure IdSimps = Named_Thms
   205 structure IdSimps = Named_Thms
   198   (val name = "id_simps"
   206   (val name = "id_simps"
   199    val description = "Identity simp rules for maps.")
   207    val description = "Identity simp rules for maps.")
   200 
   208 
   201 val id_simps_get = IdSimps.get
   209 val id_simps_get = IdSimps.get
   202 
   210 
   203 (* quotient theorems *)
   211 (* quotient theorems *)
   204 structure QuotientRules = Named_Thms
   212 structure QuotientRules = Named_Thms
   205   (val name = "quotient_thm"
   213   (val name = "quot_thm"
   206    val description = "Quotient theorems.")
   214    val description = "Quotient theorems.")
   207 
   215 
   208 val quotient_rules_get = QuotientRules.get
   216 val quotient_rules_get = QuotientRules.get
   209 val quotient_rules_add = QuotientRules.add
   217 val quotient_rules_add = QuotientRules.add
   210 
   218