src/HOLCF/Domain.thy
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";