src/HOL/HOLCF/Fixrec.thy
changeset 46950 d0181abdbdac
parent 42151 4da4fc77664b
child 47432 e1576d13e933
equal deleted inserted replaced
46949:94aa7b81bcf6 46950:d0181abdbdac
     4 
     4 
     5 header "Package for defining recursive functions in HOLCF"
     5 header "Package for defining recursive functions in HOLCF"
     6 
     6 
     7 theory Fixrec
     7 theory Fixrec
     8 imports Plain_HOLCF
     8 imports Plain_HOLCF
       
     9 keywords "fixrec" :: thy_decl
     9 uses
    10 uses
    10   ("Tools/holcf_library.ML")
    11   ("Tools/holcf_library.ML")
    11   ("Tools/fixrec.ML")
    12   ("Tools/fixrec.ML")
    12 begin
    13 begin
    13 
    14