blob: 5d55a2aef7dfe59df305820a597b3ed97b0d6b7b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
|
(*
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.
Assumption.
Assumption.
Save and_comms.
End sect.
Module mod.
Definition type1:=Set.
End mod.
Module Type newmod.
Definition type1:=Set.
End newmod.
|
