src/HOLCF/Cont.thy
changeset 31902 862ae16a799d
parent 31076 99fe356cbbc2
child 35794 8cd7134275cc
     1.1 --- a/src/HOLCF/Cont.thy	Thu Jul 02 17:33:36 2009 +0200
     1.2 +++ b/src/HOLCF/Cont.thy	Thu Jul 02 17:34:14 2009 +0200
     1.3 @@ -140,8 +140,11 @@
     1.4  subsection {* Continuity simproc *}
     1.5  
     1.6  ML {*
     1.7 -structure Cont2ContData = NamedThmsFun
     1.8 -  ( val name = "cont2cont" val description = "continuity intro rule" )
     1.9 +structure Cont2ContData = Named_Thms
    1.10 +(
    1.11 +  val name = "cont2cont"
    1.12 +  val description = "continuity intro rule"
    1.13 +)
    1.14  *}
    1.15  
    1.16  setup Cont2ContData.setup