src/HOL/UNITY/Rename.thy
changeset 46577 e5438c5797ae
parent 45605 a89b4bc311a5
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/UNITY/Rename.thy	Tue Feb 21 17:08:32 2012 +0100
     1.2 +++ b/src/HOL/UNITY/Rename.thy	Tue Feb 21 17:09:17 2012 +0100
     1.3 @@ -64,7 +64,7 @@
     1.4  apply (simp add: bij_extend_act_eq_project_act)
     1.5  apply (rule surjI)
     1.6  apply (rule Extend.extend_act_inverse)
     1.7 -apply (blast intro: bij_imp_bij_inv good_map_bij)
     1.8 +apply (blast intro: bij_imp_bij_inv)
     1.9  done
    1.10  
    1.11  lemma bij_project_act: "bij h ==> bij (project_act (%(x,u::'c). h x))"