7 Commits

Author	SHA1	Message	Date
Jean-Christophe Filliatre	114fc686a9	new example: Knuth's bubble sort	2024-09-05 19:11:32 +02:00
Andrei Paskevich	eae547d95f	stdlib, examples: remove redundant "import"	2018-06-15 16:45:58 +02:00
Andrei Paskevich	fb77f39422	Vc: no more "liberal_for" ... Instead, we put a "stop_split" over the subsequent postcondition under the (begin > end + 1) assumption. When this assumption is unrealizable (strict for), this allows us to discharge the whole branch as a single goal.	2017-05-22 16:28:07 +02:00
Jean-Christophe Filliatre	3766147ed1	updated proof sessions	2017-05-16 17:06:08 +02:00
Andrei Paskevich	bfc08a83ed	update a couple of sessions	2016-03-09 17:54:33 +01:00
Claude Marche	2020494503	List, Option, BinTree : test for emptiness in programs	2016-03-09 16:34:53 +01:00
Claude Marché	5bb3c2e638	New example: bubble sort	2014-07-03 06:44:10 +02:00