2 (* ---------------------------------------------------------------------- *)
4 (* ---------------------------------------------------------------------- *)
5 let dest_beq = dest_binop `(<=>)`;;
9 parse_as_infix ("<>",(12,"right"));;
11 let NEQ = new_definition
12 `x <> y <=> ~(x = y)`;;
14 let nqt = `(<>):A -> A -> bool`;;
18 let nqt' = inst[ty,aty] nqt in
19 mk_comb(mk_comb(nqt',l),r)
20 with Failure _ -> failwith "mk_neq";;
22 (* ---------------------------------------------------------------------- *)
24 (* ---------------------------------------------------------------------- *)
26 let IMP_AND_THM = TAUT `(p ==> q ==> r) <=> (p /\ q ==> r)`;;
27 let AND_IMP_THM = TAUT `(p /\ q ==> r) <=> (p ==> q ==> r)`;;
29 let is_pos tm = not (is_neg tm);;
32 end_itlist CONJ thms;;
35 CONJ_LIST [TRUTH;TRUTH;TRUTH]