equal
deleted
inserted
replaced
265 val (le1,le2) = (hd leqs, hd(tl leqs)); |
265 val (le1,le2) = (hd leqs, hd(tl leqs)); |
266 val (eq1,eq2) = (le1 RS dist_eqI, le2 RS dist_eqI) in |
266 val (eq1,eq2) = (le1 RS dist_eqI, le2 RS dist_eqI) in |
267 if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else |
267 if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else |
268 if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else |
268 if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else |
269 [eq1, eq2] end; |
269 [eq1, eq2] end; |
270 open Basis_Library (*restore original List*) |
270 open BasisLibrary (*restore original List*) |
271 fun distincts [] = [] |
271 fun distincts [] = [] |
272 | distincts ((c,leqs)::cs) = List.concat |
272 | distincts ((c,leqs)::cs) = List.concat |
273 (ListPair.map (distinct c) ((map #1 cs),leqs)) @ |
273 (ListPair.map (distinct c) ((map #1 cs),leqs)) @ |
274 distincts cs; |
274 distincts cs; |
275 in distincts (cons~~distincts_le) end; |
275 in distincts (cons~~distincts_le) end; |