changeset 35443 | 2e0f9516947e |
parent 31232 | 689aa7da48cc |
child 35444 | 73f645fdd4ff |
--- a/src/HOLCF/ex/Domain_ex.thy Wed Feb 24 14:13:15 2010 -0800 +++ b/src/HOLCF/ex/Domain_ex.thy Wed Feb 24 14:20:07 2010 -0800 @@ -99,7 +99,7 @@ text {* Trivial datatypes will produce a warning message. *} -domain triv = triv1 triv triv +domain triv = Triv triv triv -- "domain Domain_ex.triv is empty!" lemma "(x::triv) = \<bottom>" by (induct x, simp_all)