equal
deleted
inserted
replaced
227 ( |
227 ( |
228 type T = ((string * string) * thm) list * class list; |
228 type T = ((string * string) * thm) list * class list; |
229 val empty = ([], []); |
229 val empty = ([], []); |
230 val copy = I; |
230 val copy = I; |
231 val extend = I; |
231 val extend = I; |
232 fun merge _ ((alias1, classes1), (alias2, classes2)) = |
232 fun merge _ ((alias1, classes1), (alias2, classes2)) : T = |
233 (Library.merge (eq_snd Thm.eq_thm_prop) (alias1, alias2), |
233 (Library.merge (eq_snd Thm.eq_thm_prop) (alias1, alias2), |
234 Library.merge (op =) (classes1, classes2)); |
234 Library.merge (op =) (classes1, classes2)); |
235 ); |
235 ); |
236 |
236 |
237 fun add_const_alias thm thy = |
237 fun add_const_alias thm thy = |