equal
deleted
inserted
replaced
288 |
288 |
289 (** attributes **) |
289 (** attributes **) |
290 |
290 |
291 local |
291 local |
292 |
292 |
293 fun mk_att f g name arg = |
293 fun mk_att f g name = |
294 let val (x, thm) = g arg in (Data.map (f (name, thm)) x, thm) end; |
294 Thm.mixed_attribute (fn (context, thm) => |
|
295 let |
|
296 val thm' = g thm; |
|
297 val context' = Data.map (f (name, thm')) context; |
|
298 in (context', thm') end); |
295 |
299 |
296 fun del_att which = |
300 fun del_att which = |
297 Thm.declaration_attribute (fn th => Data.map (which (pairself (fn rs => |
301 Thm.declaration_attribute (fn th => Data.map (which (pairself (fn rs => |
298 fold Item_Net.remove (filter_rules rs th) rs)))); |
302 fold Item_Net.remove (filter_rules rs th) rs)))); |
299 |
303 |
307 fun add_inductT rule x = map2 (apfst (Item_Net.update rule)) x; |
311 fun add_inductT rule x = map2 (apfst (Item_Net.update rule)) x; |
308 fun add_inductP rule x = map2 (apsnd (Item_Net.update rule)) x; |
312 fun add_inductP rule x = map2 (apsnd (Item_Net.update rule)) x; |
309 fun add_coinductT rule x = map3 (apfst (Item_Net.update rule)) x; |
313 fun add_coinductT rule x = map3 (apfst (Item_Net.update rule)) x; |
310 fun add_coinductP rule x = map3 (apsnd (Item_Net.update rule)) x; |
314 fun add_coinductP rule x = map3 (apsnd (Item_Net.update rule)) x; |
311 |
315 |
312 val consumes0 = Rule_Cases.consumes_default 0; |
316 val consumes0 = Rule_Cases.default_consumes 0; |
313 val consumes1 = Rule_Cases.consumes_default 1; |
317 val consumes1 = Rule_Cases.default_consumes 1; |
314 |
318 |
315 in |
319 in |
316 |
320 |
317 val cases_type = mk_att add_casesT consumes0; |
321 val cases_type = mk_att add_casesT consumes0; |
318 val cases_pred = mk_att add_casesP consumes1; |
322 val cases_pred = mk_att add_casesP consumes1; |