summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | blanchet |

Mon, 16 Aug 2010 17:44:27 +0200 | |

changeset 38456 | 6769ccd90ad6 |

parent 38455 | 131f7c46cf2c |

child 38457 | b8760b6e7c65 |

typos in comment

--- a/src/Provers/quantifier1.ML Mon Aug 16 16:58:45 2010 +0200 +++ b/src/Provers/quantifier1.ML Mon Aug 16 17:44:27 2010 +0200 @@ -17,7 +17,7 @@ And analogously for t=x, but the eqn is not turned around! NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)"; - "!x. x=t --> P(x)" is covered by the congreunce rule for -->; + "!x. x=t --> P(x)" is covered by the congruence rule for -->; "!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule. As must be "? x. t=x & P(x)". @@ -26,7 +26,7 @@ Gries etc call this the "1 point rules" The above also works for !x1..xn. and ?x1..xn by moving the defined -qunatifier inside first, but not for nested bounded quantifiers. +quantifier inside first, but not for nested bounded quantifiers. For set comprehensions the basic permutations ... & x = t & ... -> x = t & (... & ...)