equal
deleted
inserted
replaced
1 (* Title: thm |
1 (* Title: Pure/thm.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 |
5 |
6 NO REP_CTERM!! |
6 NO REP_CTERM!! |
104 |
104 |
105 |
105 |
106 functor ThmFun (structure Logic: LOGIC and Unify: UNIFY and Pattern:PATTERN |
106 functor ThmFun (structure Logic: LOGIC and Unify: UNIFY and Pattern:PATTERN |
107 and Net:NET |
107 and Net:NET |
108 sharing type Pattern.type_sig = Unify.Sign.Type.type_sig) |
108 sharing type Pattern.type_sig = Unify.Sign.Type.type_sig) |
109 : THM = |
109 (*: THM *) (* FIXME debug *) = |
110 struct |
110 struct |
111 structure Sequence = Unify.Sequence; |
111 structure Sequence = Unify.Sequence; |
112 structure Envir = Unify.Envir; |
112 structure Envir = Unify.Envir; |
113 structure Sign = Unify.Sign; |
113 structure Sign = Unify.Sign; |
114 structure Type = Sign.Type; |
114 structure Type = Sign.Type; |