equal
deleted
inserted
replaced
162 maps_update @{type_name "list"} {mapfun = @{const_name "map"}, relfun = @{const_name "LIST_REL"}} #> |
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"}} #> |
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"}} |
164 maps_update @{type_name "fun"} {mapfun = @{const_name "fun_map"}, relfun = @{const_name "FUN_REL"}} |
165 *} |
165 *} |
166 |
166 |
167 |
|
168 ML {* quotdata_lookup @{theory} *} |
|
169 setup {* quotdata_update_thy (@{typ nat}, @{typ bool}, @{term "True"})*} |
|
170 ML {* quotdata_lookup @{theory} *} |
|
171 |
|
172 ML {* print_quotdata @{context} *} |
|
173 |
|
174 ML {* maps_lookup @{theory} @{type_name list} *} |
|
175 |
|
176 ML {* |
167 ML {* |
177 val no_vars = Thm.rule_attribute (fn context => fn th => |
168 val no_vars = Thm.rule_attribute (fn context => fn th => |
178 let |
169 let |
179 val ctxt = Variable.set_body false (Context.proof_of context); |
170 val ctxt = Variable.set_body false (Context.proof_of context); |
180 val ((_, [th']), _) = Variable.import true [th] ctxt; |
171 val ((_, [th']), _) = Variable.import true [th] ctxt; |