blob: 95a9adac1cd7b81e60c6e8ba90314e015a826dcc (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
(*
Example proof script for Coq Proof General (Coq V8 syntax).
$Id$
*)
Goal forall (A B:Prop),(A /\ B) -> (B /\ A).
intros A B.
intros H.
elim H.
split.
assumption.
assumption.
Save and_comms.
|