changeset 31754 | b5260f5272a4 |
parent 27717 | 21bbd410ba04 |
child 32988 | d1d4d7a08a66 |
--- a/src/HOL/Algebra/Bij.thy Mon Jun 22 08:17:52 2009 +0200 +++ b/src/HOL/Algebra/Bij.thy Mon Jun 22 20:59:12 2009 +0200 @@ -50,7 +50,7 @@ apply (simp add: compose_Bij) apply (simp add: id_Bij) apply (simp add: compose_Bij) - apply (blast intro: compose_assoc [symmetric] Bij_imp_funcset) + apply (blast intro: compose_assoc [symmetric] dest: Bij_imp_funcset) apply (simp add: id_Bij Bij_imp_funcset Bij_imp_extensional, simp) apply (blast intro: Bij_compose_restrict_eq restrict_Inv_Bij) done