src/HOLCF/ex/Fix2.thy
changeset 10835 f4745d77e620
parent 2570 24d7e8fb8261
child 12036 49f6c49454c2
     1.1 --- a/src/HOLCF/ex/Fix2.thy	Tue Jan 09 15:32:27 2001 +0100
     1.2 +++ b/src/HOLCF/ex/Fix2.thy	Tue Jan 09 15:36:30 2001 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4  
     1.5  rules
     1.6  
     1.7 -gix1_def "F`(gix`F) = gix`F"
     1.8 -gix2_def "F`y=y ==> gix`F << y"
     1.9 +gix1_def "F$(gix$F) = gix$F"
    1.10 +gix2_def "F$y=y ==> gix$F << y"
    1.11  
    1.12  end