# HG changeset patch
# User huffman
# Date 1267516490 28800
# Node ID 89b945fa0a3118b55279092ec86cb7d26d0a2719
# Parent  5d200f2d7a4fd35961c3923cb6332ec8dbc61218
need to explicitly include REP_convex

diff -r 5d200f2d7a4f -r 89b945fa0a31 src/HOLCF/ex/Domain_Proofs.thy
--- a/src/HOLCF/ex/Domain_Proofs.thy	Mon Mar 01 19:18:08 2010 -0800
+++ b/src/HOLCF/ex/Domain_Proofs.thy	Mon Mar 01 23:54:50 2010 -0800
@@ -196,7 +196,7 @@
 by (rule bar_defl_unfold)
 
 lemma REP_baz': "REP('a baz) = REP(('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>)"
-unfolding REP_foo REP_bar REP_baz REP_simps
+unfolding REP_foo REP_bar REP_baz REP_simps REP_convex
 by (rule baz_defl_unfold)
 
 (********************************************************************)