src/HOL/UNITY/Rename.thy
changeset 45605 a89b4bc311a5
parent 40702 cf26dd7395e4
child 46577 e5438c5797ae
     1.1 --- a/src/HOL/UNITY/Rename.thy	Sun Nov 20 20:59:30 2011 +0100
     1.2 +++ b/src/HOL/UNITY/Rename.thy	Sun Nov 20 21:05:23 2011 +0100
     1.3 @@ -140,7 +140,7 @@
     1.4  lemma bij_rename: "bij h ==> bij (rename h)"
     1.5  apply (simp (no_asm_simp) add: rename_def bij_extend)
     1.6  done
     1.7 -lemmas surj_rename = bij_rename [THEN bij_is_surj, standard]
     1.8 +lemmas surj_rename = bij_rename [THEN bij_is_surj]
     1.9  
    1.10  lemma inj_rename_imp_inj: "inj (rename h) ==> inj h"
    1.11  apply (unfold inj_on_def, auto)