equal
deleted
inserted
replaced
163 ( |
163 ( |
164 type T = thm list |
164 type T = thm list |
165 val empty = [] |
165 val empty = [] |
166 val copy = I |
166 val copy = I |
167 val extend = I |
167 val extend = I |
168 fun merge _ = Library.gen_union Thm.eq_thm |
168 fun merge _ = Library.union Thm.eq_thm |
169 ) |
169 ) |
170 |
170 |
171 val hol4_debug = Unsynchronized.ref false |
171 val hol4_debug = Unsynchronized.ref false |
172 fun message s = if !hol4_debug then writeln s else () |
172 fun message s = if !hol4_debug then writeln s else () |
173 |
173 |