hol-light/TacticRecording/xthm.ml


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
31
32
33
34
35
36
37
38
39
40


(* ** DATATYPE ** *)


(* The 'xthm' datatype *)

(* This couples a theorem with an 'mldata' representation of its proof.  For  *)
(* named ML objects, this 'mldata' will simply be the ML name of the theorem. *)
(* For rule applications, it will capture the rule and its arguments.         *)

type xthm = thm * mldata;;

type xconv = term -> xthm;;


(* Constructors and destructors *)

let mk_xthm (xth:thm*mldata) : xthm = xth;;

let mk_xthm0 x th = mk_xthm (th, (x,[]));;

let dest_xthm ((th,prf):xthm) : thm * mldata = (th,prf);;

let xthm_thm ((th,_):xthm) = th;;

let xthm_proof ((_,prf):xthm) = prf;;

let name_xthm x ((th,_):xthm) : xthm = (th, (x,[]));;


(* ** INSTALL PRINTERS ** *)


let print_xthm ((th,_):xthm) = print_thm th;;

#install_printer print_xthm;;