diff options
Diffstat (limited to 'theories/Init/Logic.v')
| -rw-r--r-- | theories/Init/Logic.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 804784b30e..9251d00ff3 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -21,6 +21,9 @@ 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. |