src/HOLCF/ex/Dagstuhl.thy
changeset 10835 f4745d77e620
parent 2570 24d7e8fb8261
child 17291 94f6113fe9ed
     1.1 --- a/src/HOLCF/ex/Dagstuhl.thy	Tue Jan 09 15:32:27 2001 +0100
     1.2 +++ b/src/HOLCF/ex/Dagstuhl.thy	Tue Jan 09 15:36:30 2001 +0100
     1.3 @@ -10,8 +10,8 @@
     1.4  
     1.5  defs
     1.6  
     1.7 -YS_def    "YS  == fix`(LAM x. y && x)"
     1.8 -YYS_def   "YYS == fix`(LAM z. y && y && z)"
     1.9 +YS_def    "YS  == fix$(LAM x. y && x)"
    1.10 +YYS_def   "YYS == fix$(LAM z. y && y && z)"
    1.11    
    1.12  end
    1.13