author | wenzelm |
Tue, 25 Mar 2008 19:39:58 +0100 | |
changeset 26392 | 748b263f0e40 |
parent 26391 | 6e8aa5a4eb82 |
child 26393 | 42febbed5460 |
--- a/src/Pure/assumption.ML Tue Mar 25 19:39:57 2008 +0100 +++ b/src/Pure/assumption.ML Tue Mar 25 19:39:58 2008 +0100 @@ -76,6 +76,13 @@ fun extra_hyps ctxt th = subtract (op aconv) (map Thm.term_of (assms_of ctxt)) (Thm.hyps_of th); +(* named prems -- legacy feature *) + +val _ = Context.add_setup + (PureThy.add_thms_dynamic ("prems", + fn Context.Theory _ => [] | Context.Proof ctxt => prems_of ctxt)); + + (* add assumptions *) fun add_assms export new_asms =