equal
deleted
inserted
replaced
954 (* resolving with R x y assumptions *) |
954 (* resolving with R x y assumptions *) |
955 NDT ctxt "E" (atac) |
955 NDT ctxt "E" (atac) |
956 |
956 |
957 (* (op =) ===> (op =) \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *) |
957 (* (op =) ===> (op =) \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *) |
958 (* global simplification *) |
958 (* global simplification *) |
959 (*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]})))*) |
959 (*NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms FUN_REL_EQ LIST_REL_EQ})))*) |
960 ]) |
960 ]) |
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 = |