Lines Matching refs:same
354 (* not same as polyDivideTheory.poly_unit_property (which specifies upoly u instead of just poly u):
560 val _ = set_fixity "pdivides" (Infix(NONASSOC, 450)); (* same as relation *)
692 (* Another proof of the same theorem, with p, q interchanged. *)
713 (* Third proof of the same theorem. *)
1074 (* Original proof of the same theorem *)
1241 (* Original proof of the same theorem *)
1346 (* Original proof of the same theorem. *)
1421 (* Original proof of the same theorem. *)
1547 (* This is the same as poly_divides_mult, different proof. *)
1992 val _ = set_fixity "=~" (Infix(NONASSOC, 450)); (* same as relation *)
2090 val _ = set_fixity "~~" (Infix(NONASSOC, 450)); (* same as relation *)