src/HOLCF/ex/Dagstuhl.ML
changeset 896 56b9c2626e81
parent 895 7a1e07fbffea
child 897 55d15c603e3a
equal deleted inserted replaced
895:7a1e07fbffea 896:56b9c2626e81
     1 (*
     1 (* $Id$ *)
     2     ID:         $Id$
       
     3 *)
       
     4 
       
     5 
     2 
     6 open Dagstuhl;
     3 open Dagstuhl;
     7 
     4 
     8 val YS_def2  = fix_prover Dagstuhl.thy  YS_def  "YS  = scons[y][YS]";
     5 val YS_def2  = fix_prover Dagstuhl.thy  YS_def  "YS  = scons[y][YS]";
     9 val YYS_def2 = fix_prover Dagstuhl.thy YYS_def "YYS = scons[y][scons[y][YYS]]";
     6 val YYS_def2 = fix_prover Dagstuhl.thy YYS_def "YYS = scons[y][scons[y][YYS]]";