diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2003-10-05 15:57:35 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2003-10-05 15:57:35 +0000 |
commit | 45687f7f1ca127e881a80978f290b565ca629cf8 (patch) | |
tree | 21150b9a3d1b038269645e0d34034cb35161cea1 /coq | |
parent | 4936304bda8f1fed11aafd828be421eaf688a75d (diff) |
Rever to simplest example
Diffstat (limited to 'coq')
-rw-r--r-- | coq/example.v | 33 |
1 files changed, 1 insertions, 32 deletions
diff --git a/coq/example.v b/coq/example.v index 5d076280..d9976ea7 100644 --- a/coq/example.v +++ b/coq/example.v @@ -1,45 +1,14 @@ (* Example proof script for Coq Proof General. - This is a legal script for coq 7.x, with - imbricated proofs definitions. - - Replace Section by Module (>= coq-7.4). - $Id$ *) -Section sect. - Goal (A,B:Prop)(A /\ B) -> (B /\ A). Intros A B H. -Recursive Tactic Definition bar := Idtac. Elim H. Intros. - Lemma foo: (A:Set)Set. - Intro A. - Exact A. - Save. - Split. + Split. Assumption. Assumption. Save and_comms. -End sect. - -Section newmod. -Definition type1:=Set. - -Axiom A:False. -Goal (n:nat)(S n)=n. -Apply False_ind. -Exact A. -Save toto. -End newmod. - -Extract Constant - -Lemma Lem : (S O)=O. -AutoRewrite [db]. - -Hint Rewrite [toto] in db. -AutoRewrite [db]. |