Claude Marche 01f80d6f50 relax hypothesis on a_max

2025-12-08 16:19:47 +01:00

..

add_sqrt

Upgrade sessions to use Alt-Ergo 2.6.0

2025-01-14 19:48:35 +01:00

add_sub_mul

SLSE full proof

2025-03-10 16:00:09 +01:00

addition

fix proofs in subdir numeric

2025-09-30 13:34:10 +02:00

exp_log

Improve numeric examples on exp and log

2025-10-08 12:18:30 +02:00

log-sum-exp

relax hypothesis on a_max

2025-12-08 16:19:47 +01:00

lse

fix proofs in subdir numeric

2025-09-30 13:34:10 +02:00

multiplication

Upgrade sessions to use Alt-Ergo 2.6.0

2025-01-14 19:48:35 +01:00

sin_cos

Upgrade sessions to use Alt-Ergo 2.6.0

2025-01-14 19:48:35 +01:00

substraction

Upgrade sessions to use Alt-Ergo 2.6.0

2025-01-14 19:48:35 +01:00

sum

Upgrade sessions to use Alt-Ergo 2.6.0

2025-01-14 19:48:35 +01:00

add_sqrt.mlw

clarify ghost and non-ghost for reals and ufloats

2024-10-01 15:38:42 +02:00

add_sub_mul.mlw

clarify ghost and non-ghost for reals and ufloats

2024-10-01 15:38:42 +02:00

addition.mlw

fix proofs in subdir numeric

2025-09-30 13:34:10 +02:00

exp_log.mlw

Improve numeric examples on exp and log

2025-10-08 12:18:30 +02:00

log-sum-exp.mlw

relax hypothesis on a_max

2025-12-08 16:19:47 +01:00

lse.mlw

clarify ghost and non-ghost for reals and ufloats

2024-10-01 15:38:42 +02:00

multiplication.mlw

clarify ghost and non-ghost for reals and ufloats

2024-10-01 15:38:42 +02:00

sin_cos.mlw

clarify ghost and non-ghost for reals and ufloats

2024-10-01 15:38:42 +02:00

substraction.mlw

clarify ghost and non-ghost for reals and ufloats

2024-10-01 15:38:42 +02:00

sum.mlw

clarify ghost and non-ghost for reals and ufloats

2024-10-01 15:38:42 +02:00