blob: 7e008eb883d2dad4af308ac2398e08e06373fa24 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
(*
Example proof script for HOL Proof General.
$Id$
*)
g `A /\ B ==> B /\ A`;
e DISCH_TAC;
e CONJ_TAC;
e (IMP_RES_TAC AND_INTRO_THM);
e (IMP_RES_TAC AND_INTRO_THM);
val and_comms = pg_top_thm_and_drop();
(* Hints about HOL Proof General:
Proof General needs to work with top-level declarations throughout,
and with "interactive" rather than "batch" versions of proofs.
For best results, theorems should be saved in the way that they are
saved above, with pg_top_thm_and_drop. The function isn't
mysterious, it is defined as:
fun pg_top_thm_and_drop () = let val t = top_thm(); in (drop(); t) end;
*)
(* this simple proof is not quite like proofs in the other systems,
can anyone tell me a more similar proof in HOL? I want to split
the IMP_RES_TAC into two steps.
*)
|
