src/HOLCF/ex/Strict_Fun.thy
changeset 35479 dffffe36344a
parent 35167 eba22d68a0a7
child 35547 991a6af75978
     1.1 --- a/src/HOLCF/ex/Strict_Fun.thy	Sun Feb 28 18:12:08 2010 -0800
     1.2 +++ b/src/HOLCF/ex/Strict_Fun.thy	Sun Feb 28 18:33:57 2010 -0800
     1.3 @@ -232,8 +232,8 @@
     1.4  
     1.5  setup {*
     1.6    Domain_Isomorphism.add_type_constructor
     1.7 -    (@{type_name "sfun"}, @{term sfun_defl}, @{const_name sfun_map},
     1.8 -        @{thm REP_sfun}, @{thm isodefl_sfun}, @{thm sfun_map_ID})
     1.9 +    (@{type_name "sfun"}, @{term sfun_defl}, @{const_name sfun_map}, @{thm REP_sfun},
    1.10 +       @{thm isodefl_sfun}, @{thm sfun_map_ID}, @{thm deflation_sfun_map})
    1.11  *}
    1.12  
    1.13  end