equal
deleted
inserted
replaced
240 setup {* Sign.add_const_constraint |
240 setup {* Sign.add_const_constraint |
241 (@{const_name "permute"}, SOME @{typ "perm \<Rightarrow> 'a::pt \<Rightarrow> 'a"}) *} |
241 (@{const_name "permute"}, SOME @{typ "perm \<Rightarrow> 'a::pt \<Rightarrow> 'a"}) *} |
242 setup {* Sign.add_const_constraint |
242 setup {* Sign.add_const_constraint |
243 (@{const_name "atom"}, SOME @{typ "'a::at_base \<Rightarrow> atom"}) *} |
243 (@{const_name "atom"}, SOME @{typ "'a::at_base \<Rightarrow> atom"}) *} |
244 |
244 |
|
245 ML {* |
|
246 Theory_Target.instantiation; |
|
247 Local_Theory.exit_global |
|
248 *} |
|
249 |
245 |
250 |
246 section {* Automation for creating concrete atom types *} |
251 section {* Automation for creating concrete atom types *} |
247 |
252 |
248 text {* at the moment only single-sort concrete atoms are supported *} |
253 text {* at the moment only single-sort concrete atoms are supported *} |
249 |
254 |
250 use "nominal_atoms.ML" |
255 use "nominal_atoms.ML" |
251 |
256 |
252 |
257 |
253 |
|
254 |
|
255 end |
258 end |