src/HOL/UNITY/Extend.ML

--- a/src/HOL/UNITY/Extend.ML	Wed Feb 09 11:43:53 2000 +0100
+++ b/src/HOL/UNITY/Extend.ML	Wed Feb 09 11:45:10 2000 +0100
@@ -203,6 +203,9 @@
 
 (*** extend_act ***)
 
+(*Can't strengthen it to
+  ((h(s,y), h(s',y')) : extend_act h act) = ((s, s') : act & y=y')
+  because h doesn't have to be injective in the 2nd argument*)
 Goalw [extend_act_def]
      "((h(s,y), h(s',y)) : extend_act h act) = ((s, s') : act)";
 by Auto_tac;