302 ML {* val consts = lookup_quot_consts defs *}

   302 ML {* val consts = lookup_quot_consts defs *}

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

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

   304 

   304 

   305 thm m1

   305 thm m1

   306 

   306 

   308 lemma "IN x EMPTY = False"

   307 lemma "IN x EMPTY = False"

   309 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})

   308 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})

   310 apply(tactic {* regularize_tac @{context}  [rel_eqv] 1 *})

   309 apply(tactic {* regularize_tac @{context}  [rel_eqv] 1 *})

   311 apply(tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})

   310 apply(tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})

   312 apply(tactic {* clean_tac @{context} [quot] defs 1*})

   311 apply(tactic {* clean_tac @{context} [quot] defs 1*})