224   apply(lifting prod.induct[where 'a="atom set" and 'b="'a"])

   224   apply(lifting prod.induct[where 'a="atom set" and 'b="'a"])

   225   done

   225   done

   226 

   226 

   227 (* TEST case *)

   227 (* TEST case *)

   228 lemmas abs_induct2 = prod.induct[where 'a="atom set" and 'b="'a::pt", quot_lifted]

   228 lemmas abs_induct2 = prod.induct[where 'a="atom set" and 'b="'a::pt", quot_lifted]

   230 thm abs_induct abs_induct2

   229 thm abs_induct abs_induct2

   231 

   230 

   232 instantiation abs :: (pt) pt

   231 instantiation abs :: (pt) pt

   233 begin

   232 begin

   234 

   233