equal
deleted
inserted
replaced
955 (* resolving with R x y assumptions *) |
955 (* resolving with R x y assumptions *) |
956 NDT ctxt "E" (atac), |
956 NDT ctxt "E" (atac), |
957 |
957 |
958 (* (op =) ===> (op =) \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *) |
958 (* (op =) ===> (op =) \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *) |
959 (* global simplification *) |
959 (* global simplification *) |
960 NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))]) |
960 NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ] eq_reflection[OF LIST_REL_EQ]})))]) |
961 *} |
961 *} |
962 |
962 |
963 ML {* |
963 ML {* |
964 fun all_inj_repabs_tac ctxt rel_refl trans2 = |
964 fun all_inj_repabs_tac ctxt rel_refl trans2 = |
965 REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2) |
965 REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2) |