src/HOLCF/One.thy
changeset 1274 ea0668a1c0ba
parent 1168 74be52691d62
child 1479 21eb5e156d91
     1.1 --- a/src/HOLCF/One.thy	Fri Oct 06 16:17:08 1995 +0100
     1.2 +++ b/src/HOLCF/One.thy	Fri Oct 06 17:25:24 1995 +0100
     1.3 @@ -35,6 +35,10 @@
     1.4  defs
     1.5    one_def	"one == abs_one`(up`UU)"
     1.6    one_when_def "one_when == (LAM c u.lift`(LAM x.c)`(rep_one`u))"
     1.7 +
     1.8 +translations
     1.9 +  "case l of one => t1" == "one_when`t1`l"
    1.10 +
    1.11  end
    1.12  
    1.13