src/HOL/Tools/BNF/bnf_comp.ML
changeset 56010 abf4879d39f1
parent 55937 18e52e8c6300
child 56012 158dc03db8be
equal deleted inserted replaced
56009:dda076a32aea 56010:abf4879d39f1
     3     Author:     Jasmin Blanchette, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4     Copyright   2012
     4     Copyright   2012
     5 
     5 
     6 Composition of bounded natural functors.
     6 Composition of bounded natural functors.
     7 *)
     7 *)
     8 
       
     9 val inline_ref = Unsynchronized.ref true;
       
    10 
     8 
    11 signature BNF_COMP =
     9 signature BNF_COMP =
    12 sig
    10 sig
    13   val ID_bnf: BNF_Def.bnf
    11   val ID_bnf: BNF_Def.bnf
    14   val DEADID_bnf: BNF_Def.bnf
    12   val DEADID_bnf: BNF_Def.bnf