src/HOLCF/ex/ROOT.ML
changeset 40774 0437dbc127b3
parent 40773 6c12f5e24e34
child 40775 ed7a4eadb2f6
equal deleted inserted replaced
40773:6c12f5e24e34 40774:0437dbc127b3
     1 (*  Title:      HOLCF/ex/ROOT.ML
       
     2 
       
     3 Misc HOLCF examples.
       
     4 *)
       
     5 
       
     6 use_thys ["Dnat", "Dagstuhl", "Focus_ex", "Fix2", "Hoare",
       
     7   "Loop", "Powerdomain_ex", "Domain_Proofs",
       
     8   "Letrec",
       
     9   "Pattern_Match"];