equal
deleted
inserted
replaced
283 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) |
283 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) |
284 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
284 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
285 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
285 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
286 apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int]) |
286 apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int]) |
287 apply(simp only: nil_prs) |
287 apply(simp only: nil_prs) |
288 apply(rule test_all_prs) |
|
289 apply(tactic {* rtac quot 1 *}) |
|
290 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
288 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
291 done |
289 done |
292 |
290 |
293 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)" |
291 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)" |
294 sorry |
292 sorry |