equal
deleted
inserted
replaced
2568 |
2568 |
2569 val timer = time (timer "relator coinduction"); |
2569 val timer = time (timer "relator coinduction"); |
2570 |
2570 |
2571 val common_notes = |
2571 val common_notes = |
2572 [(dtor_coinductN, [dtor_coinduct_thm]), |
2572 [(dtor_coinductN, [dtor_coinduct_thm]), |
2573 (rel_coinductN, [Jrel_coinduct_thm]), |
2573 (dtor_rel_coinductN, [Jrel_coinduct_thm]), |
2574 (dtor_unfold_transferN, dtor_unfold_transfer_thms)] |
2574 (dtor_unfold_transferN, dtor_unfold_transfer_thms)] |
2575 |> map (fn (thmN, thms) => |
2575 |> map (fn (thmN, thms) => |
2576 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); |
2576 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); |
2577 |
2577 |
2578 val notes = |
2578 val notes = |