--- a/src/HOL/Finite_Set.thy Thu Jun 12 11:51:47 2008 +0200
+++ b/src/HOL/Finite_Set.thy Thu Jun 12 14:10:41 2008 +0200
@@ -535,7 +535,7 @@
have nSuc: "n = Suc m" by fact
have mlessn: "m<n" by (simp add: nSuc)
from aA obtain k where hkeq: "h k = a" and klessn: "k<n" by (blast elim!: equalityE)
- let ?hm = "swap k m h"
+ let ?hm = "Fun.swap k m h"
have inj_hm: "inj_on ?hm {i. i < n}" using klessn mlessn
by (simp add: inj_on_swap_iff inj_on)
show ?thesis
@@ -545,7 +545,7 @@
show "m<n" by (rule mlessn)
show "A = ?hm ` {i. i < m}"
proof (rule insert_image_inj_on_eq)
- show "inj_on (swap k m h) {i. i < Suc m}" using inj_hm nSuc by simp
+ show "inj_on (Fun.swap k m h) {i. i < Suc m}" using inj_hm nSuc by simp
show "?hm m \<notin> A" by (simp add: swap_def hkeq anot)
show "insert (?hm m) A = ?hm ` {i. i < Suc m}"
using aA hkeq nSuc klessn
--- a/src/HOL/Fun.thy Thu Jun 12 11:51:47 2008 +0200
+++ b/src/HOL/Fun.thy Thu Jun 12 14:10:41 2008 +0200
@@ -460,7 +460,7 @@
thus "inj_on f A" by simp
next
assume "inj_on f A"
- with A show "inj_on (swap a b f) A" by (iprover intro: inj_on_imp_inj_on_swap)
+ with A show "inj_on (swap a b f) A" by(iprover intro: inj_on_imp_inj_on_swap)
qed
lemma surj_imp_surj_swap: "surj f ==> surj (swap a b f)"
@@ -482,6 +482,7 @@
lemma bij_swap_iff: "bij (swap a b f) = bij f"
by (simp add: bij_def)
+hide const swap
subsection {* Proof tool setup *}