# HG changeset patch
# User paulson
# Date 919675225 -3600
# Node ID 062aa156a300220600592430789a35c5651b3f36
# Parent  694c9c1910e82d5eb5b408410b44632bd863c176
added a commment on the "ext" rule

diff -r 694c9c1910e8 -r 062aa156a300 src/HOL/HOL.thy
--- 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"