equal
deleted
inserted
replaced
670 |
670 |
671 fun filter_prems_tac_items (p : term -> bool) (terms : term list) : term list = |
671 fun filter_prems_tac_items (p : term -> bool) (terms : term list) : term list = |
672 let |
672 let |
673 fun filter_prems (t, (left, right)) = |
673 fun filter_prems (t, (left, right)) = |
674 if p t then (left, right @ [t]) else (left @ right, []) |
674 if p t then (left, right @ [t]) else (left @ right, []) |
675 val (left, right) = foldl filter_prems ([], []) terms |
675 val (left, right) = List.foldl filter_prems ([], []) terms |
676 in |
676 in |
677 right @ left |
677 right @ left |
678 end; |
678 end; |
679 |
679 |
680 (* return true iff TRY (etac notE) THEN eq_assume_tac would succeed on a *) |
680 (* return true iff TRY (etac notE) THEN eq_assume_tac would succeed on a *) |