Lines Matching refs:Def
69 let Def = definition `dataabs` `Def`;;
79 Def (i t) ==>
80 Def (o t) /\ (BoolAbs (o t) = inv (BoolAbs (i t)))",
85 PURE_REWRITE_TAC [Def] THEN
95 Def (i1 t) /\ Def (i2 t) ==>
96 Def (o t) /\
102 PURE_REWRITE_TAC [Def] THEN
112 Def (i1 t) /\ Def (i2 t) ==>
113 Def (o t) /\
129 Def (i1 t) /\ Def (i2 t) ==>
130 Def (o t) /\