--- a/src/HOL/HOLCF/Domain.thy Fri Aug 15 18:02:34 2014 +0200
+++ b/src/HOL/HOLCF/Domain.thy Sat Aug 16 11:35:33 2014 +0200
@@ -316,12 +316,13 @@
subsection {* Setting up the domain package *}
+named_theorems domain_defl_simps "theorems like DEFL('a t) = t_defl$DEFL('a)"
+named_theorems domain_isodefl "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)"
+
ML_file "Tools/Domain/domain_isomorphism.ML"
ML_file "Tools/Domain/domain_axioms.ML"
ML_file "Tools/Domain/domain.ML"
-setup Domain_Isomorphism.setup
-
lemmas [domain_defl_simps] =
DEFL_cfun DEFL_sfun DEFL_ssum DEFL_sprod DEFL_prod DEFL_u
liftdefl_eq LIFTDEFL_prod u_liftdefl_liftdefl_of