equal
deleted
inserted
replaced
41 val strip_prems: int * term list * term -> term list * term |
41 val strip_prems: int * term list * term -> term list * term |
42 val thaw_vars: term -> term |
42 val thaw_vars: term -> term |
43 val varify: term -> term |
43 val varify: term -> term |
44 end; |
44 end; |
45 |
45 |
46 functor LogicFun (structure Unify: UNIFY and Net:NET) : LOGIC = |
46 functor LogicFun (structure Unify: UNIFY and Net:NET)(* : LOGIC *) = (* FIXME *) |
47 struct |
47 struct |
48 structure Type = Unify.Sign.Type; |
48 structure Type = Unify.Sign.Type; |
49 |
49 |
50 (*** Abstract syntax operations on the meta-connectives ***) |
50 (*** Abstract syntax operations on the meta-connectives ***) |
51 |
51 |