diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-08 18:50:59 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-08 18:50:59 +0000 |
| commit | 1f48326c7edf7f6e7062633494d25b254a6db82c (patch) | |
| tree | ad4abb42a890edb8a0f5c92bc658e0a26b365526 /theories/Init/Logic.v | |
| parent | 9ea680a275d3a93a35c3f09f53f26ee74d51fb00 (diff) | |
Side effect free implementation of admit (Isabelle's oracle)
new Axiom in Logic.v, proof_admitted : False.
admit now simply cases proof_admitted and does
not create a new Axiom in the environment.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16673 85f007b7-540e-0410-9357-904b9bb8a0f7
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 804784b30..9251d00ff 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. |