equal
deleted
inserted
replaced
316 |
316 |
317 |
317 |
318 apply (tactic {* clean_tac @{context} defs aps 1 *}) |
318 apply (tactic {* clean_tac @{context} defs aps 1 *}) |
319 ML_prf {* *} |
319 ML_prf {* *} |
320 print_quotients |
320 print_quotients |
321 apply(tactic {* r_mk_comb_tac' @{context} rty [quot] rel_refl trans2 [] 1*}) |
321 apply(tactic {* r_mk_comb_tac' @{context} rty [quot] rel_refl [trans2] [] 1*}) |
322 |
322 |
323 |
323 |
324 ML {* val consts = lookup_quot_consts defs *} |
324 ML {* val consts = lookup_quot_consts defs *} |
325 |
325 |
326 ML {* |
326 ML {* |