- | Use_ring_Luke -> sprintf "<ring />"
- | Use_fourier_Luke -> sprintf "<fourier />"
- | Use_reflexivity_Luke -> sprintf "<reflexivity />"
- | Use_symmetry_Luke -> sprintf "<symmetry />"
- | Use_assumption_Luke -> sprintf "<assumption />"
- | Use_contradiction_Luke -> sprintf "<contradiction />"
- | Use_exists_Luke -> sprintf "<exists />"
- | Use_split_Luke -> sprintf "<split />"
- | Use_left_Luke -> sprintf "<left />"
- | Use_right_Luke -> sprintf "<right />"
- | Use_apply_Luke term -> sprintf "<apply>%s</apply>" term
+ | Use_ring -> sprintf "<ring />"
+ | Use_fourier -> sprintf "<fourier />"
+ | Use_reflexivity -> sprintf "<reflexivity />"
+ | Use_symmetry -> sprintf "<symmetry />"
+ | Use_assumption -> sprintf "<assumption />"
+ | Use_contradiction -> sprintf "<contradiction />"
+ | Use_exists -> sprintf "<exists />"
+ | Use_split -> sprintf "<split />"
+ | Use_left -> sprintf "<left />"
+ | Use_right -> sprintf "<right />"
+ | Use_apply term -> sprintf "<apply>%s</apply>" term