hol98/example.sml


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

(*
    Example proof script for HOL Proof General.

    $Id$
*)    

g `A /\ B ==> B /\ A`;
e DISCH_TAC;
e CONJ_TAC;
 

(* Ooops, I'm stuck now.  Can somebody help?? 
   Just want a simple low-level proof here. *)