updated to named_theorems;
authorwenzelm
Sat Aug 16 20:27:51 2014 +0200 (2014-08-16)
changeset 5796110b2f60b70f0
parent 57960 ee1ba4848896
child 57962 0284a7d083be
updated to named_theorems;
src/HOL/Lifting.thy
src/HOL/Tools/Lifting/lifting_info.ML
     1.1 --- a/src/HOL/Lifting.thy	Sat Aug 16 20:14:45 2014 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Sat Aug 16 20:27:51 2014 +0200
     1.3 @@ -545,6 +545,8 @@
     1.4  
     1.5  ML_file "Tools/Lifting/lifting_util.ML"
     1.6  
     1.7 +named_theorems relator_eq_onp
     1.8 +  "theorems that a relator of an eq_onp is an eq_onp of the corresponding predicate"
     1.9  ML_file "Tools/Lifting/lifting_info.ML"
    1.10  setup Lifting_Info.setup
    1.11  
     2.1 --- a/src/HOL/Tools/Lifting/lifting_info.ML	Sat Aug 16 20:14:45 2014 +0200
     2.2 +++ b/src/HOL/Tools/Lifting/lifting_info.ML	Sat Aug 16 20:27:51 2014 +0200
     2.3 @@ -277,13 +277,8 @@
     2.4  
     2.5  (* theorems that a relator of an eq_onp is an eq_onp of the corresponding predicate *)
     2.6  
     2.7 -structure Relator_Eq_Onp = Named_Thms
     2.8 -(
     2.9 -  val name = @{binding relator_eq_onp}
    2.10 -  val description = "theorems that a relator of an eq_onp is an eq_onp of the corresponding predicate"
    2.11 -)
    2.12 -
    2.13 -fun get_relator_eq_onp_rules ctxt = map safe_mk_meta_eq (Relator_Eq_Onp.get ctxt)
    2.14 +fun get_relator_eq_onp_rules ctxt =
    2.15 +  map safe_mk_meta_eq (rev (Named_Theorems.get ctxt @{named_theorems relator_eq_onp}))
    2.16  
    2.17  (* info about reflexivity rules *)
    2.18  
    2.19 @@ -525,12 +520,13 @@
    2.20  val setup =
    2.21    quot_map_attribute_setup
    2.22    #> quot_del_attribute_setup
    2.23 -  #> Relator_Eq_Onp.setup
    2.24    #> relator_distr_attribute_setup
    2.25  
    2.26  (* setup fixed eq_onp rules *)
    2.27  
    2.28 -val _ = Context.>> (fold (Relator_Eq_Onp.add_thm o Transfer.prep_transfer_domain_thm @{context}) 
    2.29 +val _ = Context.>>
    2.30 +  (fold (Named_Theorems.add_thm @{named_theorems relator_eq_onp} o
    2.31 +    Transfer.prep_transfer_domain_thm @{context})
    2.32    @{thms composed_equiv_rel_eq_onp composed_equiv_rel_eq_eq_onp})
    2.33  
    2.34  (* setup fixed reflexivity rules *)