equal
deleted
inserted
replaced
19 |
19 |
20 "----------- fun matchsub ----------------------------------------"; |
20 "----------- fun matchsub ----------------------------------------"; |
21 "----------- fun matchsub ----------------------------------------"; |
21 "----------- fun matchsub ----------------------------------------"; |
22 "----------- fun matchsub ----------------------------------------"; |
22 "----------- fun matchsub ----------------------------------------"; |
23 if matchsub thy (str2term "(a + (b + c))") (str2term "?x + (?y + ?z)") |
23 if matchsub thy (str2term "(a + (b + c))") (str2term "?x + (?y + ?z)") |
24 then () else raise error "tools.sml matchsub a + (b + c)"; |
24 then () else error "tools.sml matchsub a + (b + c)"; |
25 |
25 |
26 if matchsub thy (str2term "(a + (b + c)) + d") (str2term "?x + (?y + ?z)") |
26 if matchsub thy (str2term "(a + (b + c)) + d") (str2term "?x + (?y + ?z)") |
27 then () else raise error "tools.sml matchsub (a + (b + c)) + d"; |
27 then () else error "tools.sml matchsub (a + (b + c)) + d"; |