equal
deleted
inserted
replaced
746 |
746 |
747 (** tactics and methods **) |
747 (** tactics and methods **) |
748 |
748 |
749 fun intro_classes_tac ctxt facts st = |
749 fun intro_classes_tac ctxt facts st = |
750 let |
750 let |
751 val thy = Thm.theory_of_thm st; |
751 val thy = Proof_Context.theory_of ctxt; |
752 val classes = Sign.all_classes thy; |
752 val classes = Sign.all_classes thy; |
753 val class_trivs = map (Thm.class_triv thy) classes; |
753 val class_trivs = map (Thm.class_triv thy) classes; |
754 val class_intros = map_filter (try (#intro o Axclass.get_info thy)) classes; |
754 val class_intros = map_filter (try (#intro o Axclass.get_info thy)) classes; |
755 val assm_intros = all_assm_intros thy; |
755 val assm_intros = all_assm_intros thy; |
756 in |
756 in |