equal
deleted
inserted
replaced
156 section {* type definition for the quotient type *} |
156 section {* type definition for the quotient type *} |
157 |
157 |
158 use "quotient.ML" |
158 use "quotient.ML" |
159 |
159 |
160 (* mapfuns for some standard types *) |
160 (* mapfuns for some standard types *) |
|
161 setup {* |
|
162 maps_update @{type_name "list"} {mapfun = @{const_name "map"}, relfun = @{const_name "LIST_REL"}} #> |
|
163 maps_update @{type_name "*"} {mapfun = @{const_name "prod_fun"}, relfun = @{const_name "prod_rel"}} #> |
|
164 maps_update @{type_name "fun"} {mapfun = @{const_name "fun_map"}, relfun = @{const_name "FUN_REL"}} |
|
165 *} |
|
166 |
161 |
167 |
162 ML {* quotdata_lookup @{theory} *} |
168 ML {* quotdata_lookup @{theory} *} |
163 setup {* quotdata_update_thy (@{typ nat}, @{typ bool}, @{term "True"})*} |
169 setup {* quotdata_update_thy (@{typ nat}, @{typ bool}, @{term "True"})*} |
164 ML {* quotdata_lookup @{theory} *} |
170 ML {* quotdata_lookup @{theory} *} |
165 |
171 |