multiplication_names « jvm « ssreflect « libs « ML4PG « coq - proof-general - Emacs plugins for proof management systems

about summary refs log tree commit diff

path: root/coq/ML4PG/libs/ssreflect/jvm/multiplication_names

blob: f3303d78e4185253fdea976a5f3725037af92928 (plain)

1 helper_mul_is_theta
2 fn_mul_is_theta
3 loop_is_helper_mul
4 program_is_fn_mul
5 program_correct_mul
6 total_correctness_mul