equal
deleted
inserted
replaced
37 in |
37 in |
38 rtac (Drule.instantiate_normalize insts rule) i |
38 rtac (Drule.instantiate_normalize insts rule) i |
39 end |
39 end |
40 handle Pattern.MATCH => no_tac |
40 handle Pattern.MATCH => no_tac |
41 |
41 |
42 val rules = @{thm is_equality_eq} :: |
42 val rules = ((Transfer.get_relator_eq_raw ctxt) @ (Lifting_Info.get_reflexivity_rules ctxt)) |
43 ((Transfer.get_relator_eq_raw ctxt) @ (Lifting_Info.get_reflexivity_rules ctxt)) |
|
44 in |
43 in |
45 EVERY' [CSUBGOAL intro_reflp_tac, |
44 EVERY' [CSUBGOAL intro_reflp_tac, |
46 REPEAT_ALL_NEW (resolve_tac rules)] |
45 REPEAT_ALL_NEW (resolve_tac rules)] |
47 end |
46 end |
48 |
47 |