src/HOL/HOL.thy
changeset 6289 062aa156a300
parent 6027 9dd06eeda95c
child 6340 7d5cbd5819a0
     1.1 --- a/src/HOL/HOL.thy	Mon Feb 22 10:19:32 1999 +0100
     1.2 +++ b/src/HOL/HOL.thy	Mon Feb 22 10:20:25 1999 +0100
     1.3 @@ -156,7 +156,12 @@
     1.4  
     1.5    refl          "t = (t::'a)"
     1.6    subst         "[| s = t; P(s) |] ==> P(t::'a)"
     1.7 +
     1.8 +  (*Extensionality is built into the meta-logic, and this rule expresses
     1.9 +    a related property.  It is an eta-expanded version of the traditional
    1.10 +    rule, and similar to the ABS rule of HOL.*)
    1.11    ext           "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
    1.12 +
    1.13    selectI       "P (x::'a) ==> P (@x. P x)"
    1.14  
    1.15    impI          "(P ==> Q) ==> P-->Q"