Commit 3de9196e authored by MARCHE Claude's avatar MARCHE Claude

minor details

parent 6e73d4fc
......@@ -119,6 +119,9 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
- API doc, produced using ocamldoc, to http://why3.lri.fr/api/
Note: check that URL of API doc is correct in doc/api.tex line 9.
- update the main HTML page (where is the sources ?)
- add links to extra resources like
http://why3.lri.fr/jfla-2012/, http://www.lri.fr/~marche/MPRI-2-36-1/,
http://proval.lri.fr/gallery/index.en.html
* produce the Why3 part of ProVal gallery ?
* Announce the distrib
- What to put in the announcement: see New Features above
......
......@@ -14,6 +14,7 @@ theory List
| Nil -> false
| Cons y r -> x = y \/ mem x r
end
end
theory SortedList
......
......@@ -36,8 +36,12 @@ Notation "x == y" := (infix_eqeq x y) (at level 70, no associativity).
Require Import FunctionalExtensionality.
(*
Require Classical.
Require ClassicalFacts.
Require PredicateExtensionality.
Require ProofIrrelevance.
*)
(* DO NOT EDIT BELOW *)
Lemma extensionality : forall (a:Type), forall (s1:(set a)) (s2:(set a)),
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment