equal
deleted
inserted
replaced
95 (* open FocusTermFUN( structure EncodeTerm = EncodeIsaFTerm ); *) |
95 (* open FocusTermFUN( structure EncodeTerm = EncodeIsaFTerm ); *) |
96 |
96 |
97 open BasicIsaFTerm; |
97 open BasicIsaFTerm; |
98 |
98 |
99 |
99 |
100 (* SOME general search within a focus term... *) |
100 (* Some general search within a focus term... *) |
101 |
101 |
102 (* Note: only upterms with a free or constant are going to yeald a |
102 (* Note: only upterms with a free or constant are going to yeald a |
103 match, thus if we get anything else (bound or var) skip it! This is |
103 match, thus if we get anything else (bound or var) skip it! This is |
104 important if we switch to a unification net! in particular to avoid |
104 important if we switch to a unification net! in particular to avoid |
105 vars. *) |
105 vars. *) |