20 Commits

Author	SHA1	Message	Date
Loïc Correnson	e2afddb11d	Resolve "Add injectivity for type invariant"	2024-01-31 13:02:13 +00: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
Matteo Manighetti	eddcb30d72	Update Alt-Ergo 2.3.x proofs	2023-08-28 14:17:52 +02: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
David Ewert	5f54fca95f	Add "remove_unused:dependency" to int.ComputerDivision	2022-09-21 20:15:46 +00:00
Claude Marche	db96723fd9	fix sessions	2022-07-07 15:49:23 +02:00
Claude Marche	8abedf035e	fix sessions	2022-06-02 17:59:27 +02: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
Claude Marche	fe71a8682d	fix proof using another prover	2020-08-26 10:34:25 +02:00
Jean-Christophe Filliatre	86b7a7c78a	updated proof sessions	2020-07-14 16:32:25 +02:00
Cláudio Belo Lourenço	2bf2f06f96	Update sessions using string theory.	2020-06-23 09:11:55 +02:00
Cláudio Belo Lourenço	424586aaa9	Update sessions	2020-04-03 12:30:03 +01:00
Cláudio Belo Lourenço	affea82b75	Fixes in base64 ane hex encoding	2020-02-24 16:16:39 +01:00
Jean-Christophe Filliatre	b13bca590c	updated proof sessions using strings	2020-02-20 15:28:46 +01:00
Cláudio Belo Lourenço	d5cb482a25	Moving provable lemmas into string theory as axioms	2020-02-12 16:08:42 +01:00
Cláudio Belo Lourenço	99b8d3fa46	Spliting encoding into two files	2020-02-12 15:19:54 +01:00