blob: 4795d79f8f8a83446cffedd2ee21a9bc54b772da (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
(*
Example proof script for Isabelle Proof General.
$Id$
*)
Goal "A & B --> B & A";
by (rtac impI 1);
by (etac conjE 1);
by (rtac conjI 1);
by (assume_tac 1);
by (assume_tac 1);
qed "and_comms";
Goal "(ALL x. P(x) --> Q) --> ((EX x. P(x)) --> Q)";
by (blast_tac (claset()) 1);
qed "";
|