305 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *}

   305 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *}

   306 ML {* val consts = lookup_quot_consts defs *}

   306 ML {* val consts = lookup_quot_consts defs *}

   307 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs *}

   307 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs *}

   308 

   308 

   309 lemma "IN x EMPTY = False"

   309 lemma "IN x EMPTY = False"

   312 

   311 

   313 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"

   312 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"

   314 by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *})

   313 by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *})

   315 

   314 

   316 lemma "INSERT a (INSERT a x) = INSERT a x"

   315 lemma "INSERT a (INSERT a x) = INSERT a x"