--- a/src/HOLCF/Domain.thy Tue Nov 16 15:29:01 2010 +0100
+++ b/src/HOLCF/Domain.thy Tue Nov 16 11:50:05 2010 -0800
@@ -7,7 +7,7 @@
theory Domain
imports Bifinite Domain_Aux
uses
- ("Tools/repdef.ML")
+ ("Tools/domaindef.ML")
("Tools/Domain/domain_isomorphism.ML")
("Tools/Domain/domain_axioms.ML")
("Tools/Domain/domain.ML")
@@ -94,7 +94,7 @@
, (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::pcpo u"}) ]
*}
-lemma typedef_rep_class:
+lemma typedef_liftdomain_class:
fixes Rep :: "'a::pcpo \<Rightarrow> udom"
fixes Abs :: "udom \<Rightarrow> 'a::pcpo"
fixes t :: defl
@@ -156,7 +156,7 @@
, (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::predomain u"}) ]
*}
-use "Tools/repdef.ML"
+use "Tools/domaindef.ML"
subsection {* Isomorphic deflations *}