diff options
Diffstat (limited to 'theories/Init/Logic.v')
| -rw-r--r-- | theories/Init/Logic.v | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index d2971552..50f853f0 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -22,9 +22,6 @@ Inductive True : Prop := (** [False] is the always false proposition *) Inductive False : Prop :=. -(** [proof_admitted] is used to implement the admit tactic *) -Axiom proof_admitted : False. - (** [not A], written [~A], is the negation of [A] *) Definition not (A:Prop) := A -> False. |