Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
need to explicitly include REP_convex
authorhuffman
Mon, 01 Mar 2010 23:54:50 -0800
changeset 35493 89b945fa0a31
parent 35492 5d200f2d7a4f
child 35494 45c9a8278faf
need to explicitly include REP_convex
src/HOLCF/ex/Domain_Proofs.thy file | annotate | diff | comparison | revisions 
--- 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)
 
 (********************************************************************)
isabelle