equal
deleted
inserted
replaced
466 ObjectLogic.rulify ind_r_s |
466 ObjectLogic.rulify ind_r_s |
467 end |
467 end |
468 *} |
468 *} |
469 ML fset_defs |
469 ML fset_defs |
470 |
470 |
|
471 lemma eq_r: "a = b \<Longrightarrow> a \<approx> b" |
|
472 by (simp add: list_eq_refl) |
|
473 |
471 |
474 |
472 ML {* lift @{thm m2} *} |
475 ML {* lift @{thm m2} *} |
473 ML {* lift @{thm m1} *} |
476 ML {* lift @{thm m1} *} |
474 ML {* lift @{thm list_eq.intros(4)} *} |
477 ML {* lift @{thm list_eq.intros(4)} *} |
475 ML {* lift @{thm list_eq.intros(5)} *} |
478 ML {* lift @{thm list_eq.intros(5)} *} |
476 ML {* lift @{thm card1_suc} *} |
479 ML {* lift @{thm card1_suc} *} |
477 ML {* lift @{thm map_append} *} |
480 ML {* lift @{thm map_append} *} |
478 (* ML {* lift @{thm append_assoc} *}*) |
481 ML {* lift @{thm eq_r[OF append_assoc]} *} |
479 |
482 |
480 thm |
483 thm |
481 |
484 |
482 |
485 |
483 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
486 (*notation ( output) "prop" ("#_" [1000] 1000) *) |