equal
deleted
inserted
replaced
85 |
85 |
86 |
86 |
87 functor ThmFun (structure Logic: LOGIC and Unify: UNIFY and Pattern:PATTERN |
87 functor ThmFun (structure Logic: LOGIC and Unify: UNIFY and Pattern:PATTERN |
88 and Net:NET |
88 and Net:NET |
89 sharing type Pattern.type_sig = Unify.Sign.Type.type_sig) |
89 sharing type Pattern.type_sig = Unify.Sign.Type.type_sig) |
90 : THM = |
90 (*: THM*) = (* FIXME *) |
91 struct |
91 struct |
92 structure Sequence = Unify.Sequence; |
92 structure Sequence = Unify.Sequence; |
93 structure Envir = Unify.Envir; |
93 structure Envir = Unify.Envir; |
94 structure Sign = Unify.Sign; |
94 structure Sign = Unify.Sign; |
95 structure Type = Sign.Type; |
95 structure Type = Sign.Type; |