src/HOL/HOLCF/Cont.thy
changeset 46165 3c5d3d286055
parent 43022 4da4fc77664b
child 59180 85ec71012df8
     1.1 --- a/src/HOL/HOLCF/Cont.thy	Fri Oct 28 23:16:50 2011 +0200
     1.2 +++ b/src/HOL/HOLCF/Cont.thy	Fri Oct 28 23:41:16 2011 +0200
     1.3 @@ -123,7 +123,7 @@
     1.4  ML {*
     1.5  structure Cont2ContData = Named_Thms
     1.6  (
     1.7 -  val name = "cont2cont"
     1.8 +  val name = @{binding cont2cont}
     1.9    val description = "continuity intro rule"
    1.10  )
    1.11  *}