diff -r a62cdcc5344b -r 8c9a319821b3 src/CCL/Type.thy --- a/src/CCL/Type.thy Tue Nov 11 08:57:46 2014 +0100 +++ b/src/CCL/Type.thy Tue Nov 11 10:54:52 2014 +0100 @@ -502,4 +502,8 @@ ALLGOALS EQgen_raw_tac) i *} +method_setup EQgen = {* + Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (EQgen_tac ctxt ths)) +*} + end