Commit 9e67bef2 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

set.why: remove [all : set 'a] from set.Set

The theory set.Set is used in the theory of finite sets,
but "all" is an infinite set for any infinite type.
parent fe507a04
......@@ -78,11 +78,12 @@ theory Set
axiom choose_def:
forall s: set 'a. not (is_empty s) -> mem (choose s) s
(*
(** the set of all x of type 'a *)
constant all: set 'a
axiom all_def: forall x: 'a. mem x all
*)
end
(** {2 Set Comprehension} *)
......
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