| changeset 47432 | e1576d13e933 |
| parent 47328 | 9f11a3cd84b1 |
| child 48891 | c0eafbd55de3 |
--- a/src/HOL/NSA/StarDef.thy Thu Apr 12 11:34:50 2012 +0200 +++ b/src/HOL/NSA/StarDef.thy Thu Apr 12 18:39:19 2012 +0200 @@ -91,6 +91,12 @@ use "transfer.ML" setup Transfer_Principle.setup +method_setup transfer = {* + Attrib.thms >> (fn ths => fn ctxt => + SIMPLE_METHOD' (Transfer_Principle.transfer_tac ctxt ths)) +*} "transfer principle" + + text {* Transfer introduction rules. *} lemma transfer_ex [transfer_intro]: