equal
deleted
inserted
replaced
395 |
395 |
396 |
396 |
397 (** Setup **) |
397 (** Setup **) |
398 |
398 |
399 val setup = |
399 val setup = |
400 Method.add_methods |
400 Method.setup @{binding order} (Scan.succeed (SIMPLE_METHOD' o order_tac [])) "transitivity reasoner" #> |
401 [("order", Method.ctxt_args (SIMPLE_METHOD' o order_tac []), "transitivity reasoner")] #> |
|
402 Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")]; |
401 Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")]; |
403 |
402 |
404 end; |
403 end; |
405 |
404 |
406 *} |
405 *} |