Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
changeset 41430 1aa23e9f2c87
parent 41324 1383653efec3
child 42151 4da4fc77664b 
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Jan 04 15:03:27 2011 -0800
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Jan 04 15:32:56 2011 -0800
@@ -325,7 +325,7 @@
           @{thms adm_conj adm_subst [OF _ adm_deflation]
                  cont2cont_fst cont2cont_snd cont_id}
         val bottom_rules =
-          @{thms fst_strict snd_strict deflation_UU simp_thms}
+          @{thms fst_strict snd_strict deflation_bottom simp_thms}
         val tuple_rules =
           @{thms split_def fst_conv snd_conv}
         val deflation_rules =
isabelle