equal
deleted
inserted
replaced
104 unfold_thms_tac ctxt (srel_def :: |
104 unfold_thms_tac ctxt (srel_def :: |
105 @{thms Collect_fst_snd_mem_eq mem_Collect_eq pair_mem_Collect_split fst_conv snd_conv |
105 @{thms Collect_fst_snd_mem_eq mem_Collect_eq pair_mem_Collect_split fst_conv snd_conv |
106 split_conv}) THEN |
106 split_conv}) THEN |
107 rtac refl 1; |
107 rtac refl 1; |
108 |
108 |
109 fun mk_map_comp_id_tac map_comp = |
109 fun mk_map_comp_id_tac map_comp0 = |
110 (rtac trans THEN' rtac map_comp THEN' REPEAT_DETERM o stac @{thm o_id} THEN' rtac refl) 1; |
110 (rtac trans THEN' rtac map_comp0 THEN' REPEAT_DETERM o stac @{thm o_id} THEN' rtac refl) 1; |
111 |
111 |
112 fun mk_map_cong0_tac m map_cong0 {context = ctxt, prems = _} = |
112 fun mk_map_cong0_tac m map_cong0 {context = ctxt, prems = _} = |
113 EVERY' [rtac mp, rtac map_cong0, |
113 EVERY' [rtac mp, rtac map_cong0, |
114 CONJ_WRAP' (K (rtac ballI THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1; |
114 CONJ_WRAP' (K (rtac ballI THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1; |
115 |
115 |