| changeset 17839 | 060dd0213f94 |
| parent 17836 | 5d9c9e284d16 |
| child 18487 | 4d1015084876 |
--- a/src/HOLCF/Domain.thy Wed Oct 12 03:01:09 2005 +0200 +++ b/src/HOLCF/Domain.thy Wed Oct 12 03:01:30 2005 +0200 @@ -211,6 +211,8 @@ val iso_rep_defin' = thm "iso.rep_defin'"; val iso_abs_defined = thm "iso.abs_defined"; val iso_rep_defined = thm "iso.rep_defined"; +val iso_compact_abs = thm "iso.compact_abs"; +val iso_compact_rep = thm "iso.compact_rep"; val iso_iso_swap = thm "iso.iso_swap"; val exh_start = thm "exh_start";