# HG changeset patch
# User huffman
# Date 1129078890 -7200
# Node ID 060dd0213f94ffdc1d4d4b783e92467ef2fbcab7
# Parent  3032e90c49753ffa4de2c19bf059c8ac75b9d6b1
add ML bindings for compactness lemmas

diff -r 3032e90c4975 -r 060dd0213f94 src/HOLCF/Domain.thy
--- 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";