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

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

   226   done

   226   done

   227 

   227 

   228 (* TEST case *)

   228 (* TEST case *)

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

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

   231 thm abs_induct abs_induct2

   230 thm abs_induct abs_induct2

   232 

   231 

   233 instantiation abs :: (pt) pt

   232 instantiation abs :: (pt) pt

   234 begin

   233 begin

   235 

   234