src/HOL/ex/set.thy
changeset 15481 fc075ae929e4
parent 15306 51f3d31e8eea
child 15488 7c638a46dcbb
--- a/src/HOL/ex/set.thy	Sun Jan 30 20:48:50 2005 +0100
+++ b/src/HOL/ex/set.thy	Tue Feb 01 18:01:57 2005 +0100
@@ -110,9 +110,9 @@
     apply (rule_tac [2] inj_on_inv)
     apply (erule subset_inj_on [OF _ subset_UNIV])
    txt {* Tricky variable instantiations! *}
-   apply (erule ssubst, subst double_complement)
+   apply (erule ssubst, simplesubst double_complement)
    apply (rule subsetI, erule imageE, erule ssubst, rule rangeI)
-  apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])
+  apply (erule ssubst, simplesubst double_complement, erule inv_image_comp [symmetric])
   done