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