equal
deleted
inserted
replaced
347 |
347 |
348 |
348 |
349 (* theory setup *) |
349 (* theory setup *) |
350 |
350 |
351 val _ = Context.add_setup |
351 val _ = Context.add_setup |
352 (register_config MetaSimplifier.simp_depth_limit_value #> |
352 (register_config Unify.trace_bound_value #> |
|
353 register_config Unify.search_bound_value #> |
|
354 register_config Unify.trace_simp_value #> |
|
355 register_config Unify.trace_types_value #> |
|
356 register_config MetaSimplifier.simp_depth_limit_value #> |
353 add_attributes |
357 add_attributes |
354 [("tagged", tagged, "tagged theorem"), |
358 [("tagged", tagged, "tagged theorem"), |
355 ("untagged", untagged, "untagged theorem"), |
359 ("untagged", untagged, "untagged theorem"), |
356 ("kind", kind, "theorem kind"), |
360 ("kind", kind, "theorem kind"), |
357 ("COMP", COMP_att, "direct composition with rules (no lifting)"), |
361 ("COMP", COMP_att, "direct composition with rules (no lifting)"), |