# HG changeset patch
# User wenzelm
# Date 1465568060 -7200
# Node ID 96bcd90415cbb80539241bf5341992426f2356d3
# Parent  ce63815d48dd2b66805071e26f0366b6ede565c0
tuned;

diff -r ce63815d48dd -r 96bcd90415cb src/HOL/Library/FinFun.thy
--- a/src/HOL/Library/FinFun.thy	Fri Jun 10 13:48:17 2016 +0200
+++ b/src/HOL/Library/FinFun.thy	Fri Jun 10 16:14:20 2016 +0200
@@ -189,12 +189,19 @@
   thus "curry f a \<in> finfun" unfolding finfun_def by auto
 qed
 
-bundle finfun =
-  fst_finfun[simp] snd_finfun[simp] Abs_finfun_inverse[simp] 
-  finfun_apply_inverse[simp] Abs_finfun_inject[simp] finfun_apply_inject[simp]
-  Diag_finfun[simp] finfun_curry[simp]
-  const_finfun[iff] fun_upd_finfun[iff] finfun_apply[iff] map_of_finfun[iff]
-  finfun_left_compose[intro] fst_finfun[intro] snd_finfun[intro]
+bundle finfun
+begin
+
+lemmas [simp] =
+  fst_finfun snd_finfun Abs_finfun_inverse
+  finfun_apply_inverse Abs_finfun_inject finfun_apply_inject
+  Diag_finfun finfun_curry
+lemmas [iff] =
+  const_finfun fun_upd_finfun finfun_apply map_of_finfun
+lemmas [intro] =
+  finfun_left_compose fst_finfun snd_finfun
+
+end
 
 lemma Abs_finfun_inject_finite:
   fixes x y :: "'a \<Rightarrow> 'b"
@@ -730,8 +737,8 @@
   "finite (UNIV :: 'a set) \<Longrightarrow> Finite_Set.fold (\<lambda>a. upd a b') (cnst b) (UNIV :: 'a set) = cnst b'"
 begin
 
-lemma finfun_rec_const [simp]: includes finfun shows
-  "finfun_rec cnst upd (K$ c) = cnst c"
+lemma finfun_rec_const [simp]: "finfun_rec cnst upd (K$ c) = cnst c"
+  including finfun
 proof(cases "finite (UNIV :: 'a set)")
   case False
   hence "finfun_default ((K$ c) :: 'a \<Rightarrow>f 'b) = c" by(simp add: finfun_default_const)
@@ -980,9 +987,9 @@
 by(simp add: finfun_comp2_def finfun_const_def comp_def)
 
 lemma finfun_comp2_update:
-  includes finfun
   assumes inj: "inj f"
   shows "finfun_comp2 (g(b $:= c)) f = (if b \<in> range f then (finfun_comp2 g f)(inv f b $:= c) else finfun_comp2 g f)"
+  including finfun
 proof(cases "b \<in> range f")
   case True
   from inj have "\<And>x. (op $ g)(f x := c) \<circ> f = (op $ g \<circ> f)(x := c)" by(auto intro!: ext dest: injD)