diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /theories/Sets/Powerset_Classical_facts.v | |
parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'theories/Sets/Powerset_Classical_facts.v')
-rw-r--r-- | theories/Sets/Powerset_Classical_facts.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v index 09c90506..e802beac 100644 --- a/theories/Sets/Powerset_Classical_facts.v +++ b/theories/Sets/Powerset_Classical_facts.v @@ -90,7 +90,7 @@ Section Sets_as_an_algebra. apply Subtract_intro; auto with sets. red; intro H'1; apply H'; rewrite H'1; auto with sets. Qed. - Hint Resolve incl_soustr_add_r: sets v62. + Hint Resolve incl_soustr_add_r: sets. Lemma add_soustr_2 : forall (X:Ensemble U) (x:U), @@ -328,9 +328,9 @@ Section Sets_as_an_algebra. End Sets_as_an_algebra. -Hint Resolve incl_soustr_in: sets v62. -Hint Resolve incl_soustr: sets v62. -Hint Resolve incl_soustr_add_l: sets v62. -Hint Resolve incl_soustr_add_r: sets v62. -Hint Resolve add_soustr_1 add_soustr_2: sets v62. -Hint Resolve add_soustr_xy: sets v62. +Hint Resolve incl_soustr_in: sets. +Hint Resolve incl_soustr: sets. +Hint Resolve incl_soustr_add_l: sets. +Hint Resolve incl_soustr_add_r: sets. +Hint Resolve add_soustr_1 add_soustr_2: sets. +Hint Resolve add_soustr_xy: sets. |