# HG changeset patch # User blanchet # Date 1377808786 -7200 # Node ID 7422380afe235e26dda85c9f16862ef563d629d3 # Parent f096456429848e00ae19fcd2d17c17926a4f382d compile diff -r f09645642984 -r 7422380afe23 src/HOL/BNF/More_BNFs.thy --- a/src/HOL/BNF/More_BNFs.thy Thu Aug 29 22:39:46 2013 +0200 +++ b/src/HOL/BNF/More_BNFs.thy Thu Aug 29 22:39:46 2013 +0200 @@ -227,7 +227,7 @@ apply transfer apply simp done -lemmas [simp] = fset.map_comp' fset.map_id' fset.set_map' +lemmas [simp] = fset.map_comp' fset.map_id fset.set_map' lemma fset_rel_fset: "set_rel \ (fset A1) (fset A2) = fset_rel \ A1 A2" unfolding fset_rel_def set_rel_def by auto