16 Commits

Author	SHA1	Message	Date
Claude Marche	ef62a72810	more upgraded sessions	2025-12-09 10:43:49 +01:00
Matteo Manighetti	7ae65be566	Upgrade sessions to use Alt-Ergo 2.6.0	2025-01-14 19:48:35 +01: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
Xavier Denis	87af5d805b	Initial bulk upgrade of z3	2023-04-13 09:43:18 +00:00
Claude Marche	db96723fd9	fix sessions	2022-07-07 15:49:23 +02:00
Claude Marche	33115df1c9	fix sessions	2022-06-22 15:39:14 +02:00
MARCHE Claude	c6f793011c	introduce_premises also "dequant" the let-ins	2022-04-21 16:23:20 +00:00
Claude Marche	e7efe033be	fix sessions	2021-10-30 11:11:24 +02:00
Claude Marche	62e1037ff1	fix sessions	2021-09-03 11:59:11 +02:00
Claude Marche	62d925e898	fix sessions	2021-06-25 10:26:57 +02:00
Andrei Paskevich	d2fb0befca	examples: recompute broken v6 shapes	2020-08-26 19:32:11 +02:00
Jean-Christophe Filliatre	7d23cdff04	updated proof session	2020-05-06 14:57:43 +02:00
Jean-Christophe Filliatre	11866d446d	modified example mutual_recursion	2020-05-01 21:05:40 +02:00
Jean-Christophe Filliatre	32ade6eece	examples of mutual recursion	2020-05-01 15:49:06 +02:00