src/HOL/Fun.thy
changeset 17589 58eeffd73be1
parent 17084 fb0a80aef0be
child 17877 67d5ab1cb0d8
     1.1 --- a/src/HOL/Fun.thy	Thu Sep 22 23:55:42 2005 +0200
     1.2 +++ b/src/HOL/Fun.thy	Thu Sep 22 23:56:15 2005 +0200
     1.3 @@ -429,11 +429,11 @@
     1.4  proof 
     1.5    assume "inj_on (swap a b f) A"
     1.6    with A have "inj_on (swap a b (swap a b f)) A" 
     1.7 -    by (rules intro: inj_on_imp_inj_on_swap) 
     1.8 +    by (iprover intro: inj_on_imp_inj_on_swap) 
     1.9    thus "inj_on f A" by simp 
    1.10  next
    1.11    assume "inj_on f A"
    1.12 -  with A show "inj_on (swap a b f) A" by (rules intro: inj_on_imp_inj_on_swap)
    1.13 +  with A show "inj_on (swap a b f) A" by (iprover intro: inj_on_imp_inj_on_swap)
    1.14  qed
    1.15  
    1.16  lemma surj_imp_surj_swap: "surj f ==> surj (swap a b f)"