equal
deleted
inserted
replaced
679 adding as default rewrites.*) |
679 adding as default rewrites.*) |
680 |
680 |
681 val ball_simps = map prover |
681 val ball_simps = map prover |
682 ["(ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)", |
682 ["(ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)", |
683 "(ALL x:A. P | Q x) = (P | (ALL x:A. Q x))", |
683 "(ALL x:A. P | Q x) = (P | (ALL x:A. Q x))", |
|
684 "(ALL x:A. P --> Q x) = (P --> (ALL x:A. Q x))", |
|
685 "(ALL x:A. P x --> Q) = ((EX x:A. P x) --> Q)", |
684 "(ALL x:{}. P x) = True", |
686 "(ALL x:{}. P x) = True", |
685 "(ALL x:insert a B. P x) = (P(a) & (ALL x:B. P x))", |
687 "(ALL x:insert a B. P x) = (P(a) & (ALL x:B. P x))", |
686 "(ALL x:Union(A). P x) = (ALL y:A. ALL x:y. P x)", |
688 "(ALL x:Union(A). P x) = (ALL y:A. ALL x:y. P x)", |
687 "(ALL x:Collect Q. P x) = (ALL x. Q x --> P x)"]; |
689 "(ALL x:Collect Q. P x) = (ALL x. Q x --> P x)"]; |
688 |
690 |