| changeset 20193 | 46f5ef758422 |
| parent 20140 | 98acc6d0fab6 |
| child 22846 | fb79144af9a3 |
| 20192:956cd30ef3be | 20193:46f5ef758422 |
|---|---|
502 ( |
502 ( |
503 val name = "CCL/eval"; |
503 val name = "CCL/eval"; |
504 type T = thm list; |
504 type T = thm list; |
505 val empty = []; |
505 val empty = []; |
506 val extend = I; |
506 val extend = I; |
507 fun merge _ (rules1, rules2) = gen_union Drule.eq_thm_prop (rules1, rules2); |
507 fun merge _ = Drule.merge_rules; |
508 fun print _ _ = (); |
508 fun print _ _ = (); |
509 ); |
509 ); |
510 |
510 |
511 in |
511 in |
512 |
512 |