| changeset 57961 | 10b2f60b70f0 |
| parent 57398 | 882091eb1e9a |
| child 58177 | 166131276380 |
--- a/src/HOL/Lifting.thy Sat Aug 16 20:14:45 2014 +0200 +++ b/src/HOL/Lifting.thy Sat Aug 16 20:27:51 2014 +0200 @@ -545,6 +545,8 @@ ML_file "Tools/Lifting/lifting_util.ML" +named_theorems relator_eq_onp + "theorems that a relator of an eq_onp is an eq_onp of the corresponding predicate" ML_file "Tools/Lifting/lifting_info.ML" setup Lifting_Info.setup