equal
deleted
inserted
replaced
514 #> quot_del_attribute_setup |
514 #> quot_del_attribute_setup |
515 #> Invariant_Commute.setup |
515 #> Invariant_Commute.setup |
516 #> relfexivity_rule_setup |
516 #> relfexivity_rule_setup |
517 #> relator_distr_attribute_setup |
517 #> relator_distr_attribute_setup |
518 |
518 |
|
519 (* setup fixed invariant rules *) |
|
520 |
|
521 val _ = Context.>> (fold (Invariant_Commute.add_thm o Transfer.prep_transfer_domain_thm @{context}) |
|
522 [@{thm composed_equiv_rel_invariant}, @{thm composed_equiv_rel_eq_invariant}]) |
|
523 |
519 (* outer syntax commands *) |
524 (* outer syntax commands *) |
520 |
525 |
521 val _ = |
526 val _ = |
522 Outer_Syntax.improper_command @{command_spec "print_quot_maps"} "print quotient map functions" |
527 Outer_Syntax.improper_command @{command_spec "print_quot_maps"} "print quotient map functions" |
523 (Scan.succeed (Toplevel.keep (print_quot_maps o Toplevel.context_of))) |
528 (Scan.succeed (Toplevel.keep (print_quot_maps o Toplevel.context_of))) |