equal
deleted
inserted
replaced
950 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
950 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
951 (*NDT ctxt "G" (weak_lambda_res_tac ctxt),*) |
951 (*NDT ctxt "G" (weak_lambda_res_tac ctxt),*) |
952 |
952 |
953 (* (op =) ===> (op =) \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *) |
953 (* (op =) ===> (op =) \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *) |
954 (* global simplification *) |
954 (* global simplification *) |
955 NDT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))]) |
955 NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))]) |
956 *} |
956 *} |
957 |
957 |
958 ML {* |
958 ML {* |
959 fun all_inj_repabs_tac ctxt rty quot_thms rel_refl trans2 = |
959 fun all_inj_repabs_tac ctxt rty quot_thms rel_refl trans2 = |
960 REPEAT_ALL_NEW (inj_repabs_tac ctxt rty quot_thms rel_refl trans2) |
960 REPEAT_ALL_NEW (inj_repabs_tac ctxt rty quot_thms rel_refl trans2) |