equal
deleted
inserted
replaced
646 in |
646 in |
647 simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *) |
647 simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *) |
648 THEN' RANGE (map mk_tac rthms) |
648 THEN' RANGE (map mk_tac rthms) |
649 end |
649 end |
650 |
650 |
651 (* An Attribute *) |
651 (* An Attribute which automatically constructs the qthm *) |
652 (* FIXME: Logic.unvarify needs to be replaced by propper Isar constructions *) |
652 (* FIXME: Logic.unvarify needs to be replaced by propper Isar constructions *) |
653 fun lifted_attrib_pre context thm = |
653 fun lifted_attrib_aux context thm = |
654 let |
654 let |
655 val ctxt = Context.proof_of context |
655 val ctxt = Context.proof_of context |
656 val goal = (quotient_lift_all ctxt o Logic.unvarify o prop_of) thm |
656 val goal = (quotient_lift_all ctxt o Logic.unvarify o prop_of) thm |
657 val goal_chk = Syntax.check_term ctxt goal |
657 val goal_chk = Syntax.check_term ctxt goal |
658 val frees = Term.add_free_names goal_chk [] |
658 val frees = Term.add_free_names goal_chk [] |
659 in |
659 in |
660 Goal.prove ctxt frees [] goal_chk |
660 Goal.prove ctxt frees [] goal_chk |
661 (fn x => lift_tac (#context x) [thm] 1) |
661 (fn x => lift_tac (#context x) [thm] 1) |
662 end; |
662 end; |
663 |
663 |
664 val lifted_attrib = Thm.rule_attribute lifted_attrib_pre |
664 val lifted_attrib = Thm.rule_attribute lifted_attrib_aux |
665 |
665 |
666 end; (* structure *) |
666 end; (* structure *) |