blob: 1c65ce0b440583922e8ff043d0cdd20d3f1827d0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
(*
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();;
|