--- a/src/HOLCF/Domain.thy Fri Apr 10 11:35:21 2009 -0700
+++ b/src/HOLCF/Domain.thy Fri Apr 10 17:39:53 2009 -0700
@@ -204,6 +204,15 @@
subsection {* Installing the domain package *}
+lemmas con_strict_rules =
+ sinl_strict sinr_strict spair_strict1 spair_strict2
+
+lemmas con_defin_rules =
+ sinl_defined sinr_defined spair_defined up_defined ONE_defined
+
+lemmas con_defined_iff_rules =
+ sinl_defined_iff sinr_defined_iff spair_strict_iff up_defined ONE_defined
+
use "Tools/cont_consts.ML"
use "Tools/cont_proc.ML"
use "Tools/domain/domain_library.ML"