Lines Matching defs:not
366 val not = ``$~ : bool -> bool``;
369 CONJ (REWRITE_RULE [] (AP_TERM not (SPEC_ALL FILTER_NEQ_NIL)))
370 (CONV_RULE (REWRITE_CONV [] THENC LAND_CONV SYM_CONV) (AP_TERM not (SPEC_ALL FILTER_NEQ_NIL)))
723 ``not nil = t``,
809 (* identity function. I am not sure if one should prove this fact in *)
1256 (andl [not (equal (caar a) (caadr a)) ; lexorder (caar a) (caadr a) ; sorted_car (cdr a)])
1279 val sorted_car_cons = prove(``!y x. sorted_car (cons x y) = ite (consp y) (andl [not (equal (car x) (caar y)) ; lexorder (car x) (caar y); sorted_car y]) t``,
1352 val not_pair_nil = prove(``!y f g. not (equal nil (pair f g y)) = t``,
1355 val not_nil_nil = prove(``not (equal nil nil) = nil``,
1359 ``!y x. ONE_ONE f ==> (bool (x IN FDOM y) = not (equal nil (assoc (f x) (encode_fmap f g y))))``,
1390 `ains a l = itel [(not (consp l), cons a nil) ;