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
|
(* ---------------------------------------------------------------------- *)
(* Operators *)
(* ---------------------------------------------------------------------- *)
let dest_beq = dest_binop `(<=>)`;;
let t_tm = `T`;;
let f_tm = `F`;;
parse_as_infix ("<>",(12,"right"));;
let NEQ = new_definition
`x <> y <=> ~(x = y)`;;
let nqt = `(<>):A -> A -> bool`;;
let mk_neq (l,r) =
try
let ty = type_of l in
let nqt' = inst[ty,aty] nqt in
mk_comb(mk_comb(nqt',l),r)
with Failure _ -> failwith "mk_neq";;
(* ---------------------------------------------------------------------- *)
(* Unfiled *)
(* ---------------------------------------------------------------------- *)
let IMP_AND_THM = TAUT `(p ==> q ==> r) <=> (p /\ q ==> r)`;;
let AND_IMP_THM = TAUT `(p /\ q ==> r) <=> (p ==> q ==> r)`;;
let is_pos tm = not (is_neg tm);;
let CONJ_LIST thms =
end_itlist CONJ thms;;
(*
CONJ_LIST [TRUTH;TRUTH;TRUTH]
*)
|
