| changeset 41430 | 1aa23e9f2c87 |
| parent 41413 | 64cd30d6b0b8 |
| child 41529 | ba60efa2fd08 |
--- a/src/HOL/HOLCF/Universal.thy Tue Jan 04 15:03:27 2011 -0800 +++ b/src/HOL/HOLCF/Universal.thy Tue Jan 04 15:32:56 2011 -0800 @@ -242,7 +242,7 @@ by intro_classes (fast intro: udom_minimal) lemma inst_udom_pcpo: "\<bottom> = udom_principal 0" -by (rule udom_minimal [THEN UU_I, symmetric]) +by (rule udom_minimal [THEN bottomI, symmetric]) subsection {* Compact bases of domains *}