src/HOL/Lifting.thy
changeset 57961 10b2f60b70f0
parent 57398 882091eb1e9a
child 58177 166131276380
     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