src/HOL/Lifting.thy
changeset 58821 11e226e8a095
parent 58186 a6c3962ea907
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Lifting.thy	Wed Oct 29 14:40:14 2014 +0100
     1.2 +++ b/src/HOL/Lifting.thy	Wed Oct 29 15:02:29 2014 +0100
     1.3 @@ -548,7 +548,6 @@
     1.4  named_theorems relator_eq_onp
     1.5    "theorems that a relator of an eq_onp is an eq_onp of the corresponding predicate"
     1.6  ML_file "Tools/Lifting/lifting_info.ML"
     1.7 -setup Lifting_Info.setup
     1.8  
     1.9  (* setup for the function type *)
    1.10  declare fun_quotient[quot_map]