blob: 7010fbc2267ddb77d42e147cca31b38cc9d20777 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
(*
Example proof script for HOL Proof General.
$Id$
*)
g `A /\ B ==> B /\ A`;;
e DISCH_TAC;;
e CONJ_TAC;;
e (ASM_SIMP_TAC[]);;
e (ASM_SIMP_TAC[]);;
let and_comms = top_thm();;
g `A /\ B ==> B /\ A`;;
e DISCH_TAC;;
e CONJ_TAC;;
e (ASM_SIMP_TAC[]);;
e (ASM_SIMP_TAC[]);;
let and_comms2 = top_thm();;
|