src/HOL/Lifting.thy
changeset 47777 f29e7dcd7c40
parent 47698 18202d3d5832
child 47889 29212a4bb866
     1.1 --- a/src/HOL/Lifting.thy	Thu Apr 26 01:05:06 2012 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Thu Apr 26 12:01:58 2012 +0200
     1.3 @@ -360,7 +360,7 @@
     1.4  use "Tools/Lifting/lifting_info.ML"
     1.5  setup Lifting_Info.setup
     1.6  
     1.7 -declare [[map "fun" = (fun_rel, fun_quotient)]]
     1.8 +declare fun_quotient[quot_map]
     1.9  
    1.10  use "Tools/Lifting/lifting_term.ML"
    1.11