diff -r 7a42cc191111 -r b2f32114e8a6 Quot/quotient_tacs.ML --- a/Quot/quotient_tacs.ML Fri Feb 05 10:32:21 2010 +0100 +++ b/Quot/quotient_tacs.ML Fri Feb 05 14:52:27 2010 +0100 @@ -15,6 +15,7 @@ val lift_tac: Proof.context -> thm list -> int -> tactic val quotient_tac: Proof.context -> int -> tactic val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic + val lifted_attr: attribute end; structure Quotient_Tacs: QUOTIENT_TACS = @@ -647,4 +648,15 @@ THEN' RANGE (map mk_tac rthms) end +(* The attribute *) +fun lifted_attr_pre ctxt thm = +let + val gl = (quotient_lift_all ctxt o Logic.unvarify o prop_of) thm + val glc = Syntax.check_term ctxt gl +in + (Goal.prove ctxt (Term.add_free_names glc []) [] glc (fn x => lift_tac (#context x) [thm] 1)) +end; + +val lifted_attr = Thm.rule_attribute (fn ctxt => fn t => lifted_attr_pre (Context.proof_of ctxt) t) + end; (* structure *)