equal
deleted
inserted
replaced
195 ML{*Typedef.add_typedef_global false NONE (@{binding test},[],NoSyn) |
195 ML{*Typedef.add_typedef_global false NONE (@{binding test},[],NoSyn) |
196 @{term "{1}::nat set"} NONE (simp_tac @{simpset} 1) @{theory} *} |
196 @{term "{1}::nat set"} NONE (simp_tac @{simpset} 1) @{theory} *} |
197 |
197 |
198 ML{*fun pat_completeness_auto ctxt = |
198 ML{*fun pat_completeness_auto ctxt = |
199 Pat_Completeness.pat_completeness_tac ctxt 1 |
199 Pat_Completeness.pat_completeness_tac ctxt 1 |
200 THEN auto_tac (clasimpset_of ctxt)*} |
200 THEN auto_tac ctxt*} |
201 |
201 |
202 ML {* |
202 ML {* |
203 val conf = Function_Common.default_config |
203 val conf = Function_Common.default_config |
204 *} |
204 *} |
205 |
205 |