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

author | paulson |

Mon, 22 Feb 1999 10:20:25 +0100 | |

changeset 6289 | 062aa156a300 |

parent 6288 | 694c9c1910e8 |

child 6290 | 31483ca40e91 |

added a commment on the "ext" rule

src/HOL/HOL.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/HOL.thy Mon Feb 22 10:19:32 1999 +0100 +++ b/src/HOL/HOL.thy Mon Feb 22 10:20:25 1999 +0100 @@ -156,7 +156,12 @@ refl "t = (t::'a)" subst "[| s = t; P(s) |] ==> P(t::'a)" + + (*Extensionality is built into the meta-logic, and this rule expresses + a related property. It is an eta-expanded version of the traditional + rule, and similar to the ABS rule of HOL.*) ext "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)" + selectI "P (x::'a) ==> P (@x. P x)" impI "(P ==> Q) ==> P-->Q"