fun.ML

--- a/fun.ML	Fri Jan 07 14:23:13 1994 +0100
+++ b/fun.ML	Fri Jan 14 12:35:27 1994 +0100
@@ -42,6 +42,7 @@
 
 val imageI = refl RS image_eqI;
 
+(*The eta-expansion gives variable-name preservation.*)
 val major::prems = goalw Set.thy [image_def]
     "[| b : (%x.f(x))``A;  !!x.[| b=f(x);  x:A |] ==> P |] ==> P"; 
 by (rtac (major RS CollectD RS bexE) 1);