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 |
|
250 |
|
251 section {* Automation for creating concrete atom types *} |
245 section {* Automation for creating concrete atom types *} |
252 |
246 |
253 text {* at the moment only single-sort concrete atoms are supported *} |
247 text {* at the moment only single-sort concrete atoms are supported *} |
254 |
248 |
255 use "nominal_atoms.ML" |
249 use "nominal_atoms.ML" |