src/HOL/BNF/Examples/TreeFsetI.thy
changeset 54014 21dac9a60f0c
parent 53013 3fbcfa911863
child 54027 e5853a648b59
--- a/src/HOL/BNF/Examples/TreeFsetI.thy	Tue Oct 01 17:04:27 2013 +0200
+++ b/src/HOL/BNF/Examples/TreeFsetI.thy	Tue Oct 01 17:06:35 2013 +0200
@@ -25,13 +25,13 @@
 
 lemma tmap_simps[simp]:
 "lab (tmap f t) = f (lab t)"
-"sub (tmap f t) = fmap (tmap f) (sub t)"
+"sub (tmap f t) = fimage (tmap f) (sub t)"
 unfolding tmap_def treeFsetI.sel_unfold by simp+
 
 lemma "tmap (f o g) x = tmap f (tmap g x)"
 apply (rule treeFsetI.coinduct[of "%x1 x2. \<exists>x. x1 = tmap (f o g) x \<and> x2 = tmap f (tmap g x)"])
 apply auto
-apply (unfold fset_rel_def)
+apply (unfold fset_rel_alt)
 by auto
 
 end