diff options
Diffstat (limited to 'theories/Logic/Diaconescu.v')
| -rw-r--r-- | theories/Logic/Diaconescu.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index d1327af3e9..e8e8b94ce2 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -265,7 +265,7 @@ End ProofIrrel_RelChoice_imp_EqEM. (** Proof sketch from Bell [Bell93] (with thanks to P. Castéran) *) -Notation Local inhabited A := A (only parsing). +Local Notation inhabited A := A (only parsing). Section ExtensionalEpsilon_imp_EM. @@ -279,7 +279,7 @@ Hypothesis epsilon_extensionality : forall (A:Type) (i:inhabited A) (P Q:A->Prop), (forall a, P a <-> Q a) -> epsilon A i P = epsilon A i Q. -Notation Local eps := (epsilon bool true) (only parsing). +Local Notation eps := (epsilon bool true) (only parsing). Theorem extensional_epsilon_imp_EM : forall P:Prop, P \/ ~ P. Proof. |