equal
deleted
inserted
replaced
190 |
190 |
191 section {* Definitional Packages *} |
191 section {* Definitional Packages *} |
192 |
192 |
193 text {* Type declarations *} |
193 text {* Type declarations *} |
194 |
194 |
|
195 (* |
195 ML %grayML{*Typedef.add_typedef_global (@{binding test}, [], NoSyn) |
196 ML %grayML{*Typedef.add_typedef_global (@{binding test}, [], NoSyn) |
196 @{term "{1}::nat set"} NONE (simp_tac @{context} 1) @{theory} *} |
197 @{term "{1}::nat set"} NONE (simp_tac @{context} 1) @{theory} *} |
|
198 *) |
197 |
199 |
198 ML %grayML{*fun pat_completeness_auto ctxt = |
200 ML %grayML{*fun pat_completeness_auto ctxt = |
199 Pat_Completeness.pat_completeness_tac ctxt 1 |
201 Pat_Completeness.pat_completeness_tac ctxt 1 |
200 THEN auto_tac ctxt*} |
202 THEN auto_tac ctxt*} |
201 |
203 |