11 Commits

Author	SHA1	Message	Date
Claude Marche	d818a981f2	fix cmd line for E-prover 3.x	2025-12-11 16:29:16 +01:00
Claude Marche	7620017bbf	upgraded provers in examples	2025-12-09 10:43:46 +01:00
Jean-Christophe Filliatre	cdd0075d0e	binomial coefficient example: alternative loop	2025-05-20 14:35:38 +02:00
Matteo Manighetti	7ae65be566	Upgrade sessions to use Alt-Ergo 2.6.0	2025-01-14 19:48:35 +01:00
MARCHE Claude	9161acda8e	Add metas for unused dependencies in generated axioms	2024-10-25 18:34:29 +02:00
MARCHE Claude	7e819237a6	unused dependencies on Euclidean div/mod	2024-10-23 15:10:58 +02:00
BONNOT Paul	2444f6c60a	Remove axiom CompatOrderMult from Int theory of CVCx and Z3 drivers.	2023-09-07 18:05:01 +00:00
BONNOT Paul	617b6db4e6	Resolve "Remove axioms in Z3 and CVC4 drivers"	2023-09-01 15:47:33 +00:00
BONNOT Paul	29c71dbd51	add a meta to mark a symbol as never removed by remove_unused* ... mark some lemmas on division of real as removable if not needed	2023-06-15 15:18:48 +00:00
MARCHE Claude	715fa89d16	separate transformations for intros, dequant, and remove_unused ... remove unused before reflection transformation avoid subst to a unused symbol	2023-04-25 12:20:08 +00:00
Jean-Christophe Filliatre	0efd3aa954	new example: binomial coefficient	2023-02-17 19:31:10 +01:00