| author | wneuper <Walther.Neuper@jku.at> |
| Wed, 11 Jan 2023 11:38:01 +0100 | |
| changeset 60650 | 06ec8abfd3bc |
| parent 59997 | 46fe5a8c3911 |
| permissions | -rw-r--r-- |
| neuper@41943 | 1 |
(* Title: test/../interface-xml.sml |
| neuper@41943 | 2 |
Author: Walther Neuper 110320 |
| neuper@41943 | 3 |
(c) copyright due to lincense terms. |
| neuper@41943 | 4 |
*) |
| neuper@42450 | 5 |
|
| neuper@42450 | 6 |
"-----------------------------------------------------------------"; |
| neuper@42450 | 7 |
"table of contents -----------------------------------------------"; |
| neuper@42450 | 8 |
"-----------------------------------------------------------------"; |
| neuper@42450 | 9 |
"----------- fun fetchproposedtacticOK2xml -----------------------"; |
| neuper@42450 | 10 |
"----------- fun findFillpatterns2xml ----------------------------"; |
| neuper@42450 | 11 |
"-----------------------------------------------------------------"; |
| neuper@42450 | 12 |
"-----------------------------------------------------------------"; |
| neuper@42450 | 13 |
"-----------------------------------------------------------------"; |
| neuper@42450 | 14 |
|
| neuper@42450 | 15 |
|
| neuper@42450 | 16 |
"----------- fun fetchproposedtacticOK2xml -----------------------"; |
| neuper@42450 | 17 |
"----------- fun fetchproposedtacticOK2xml -----------------------"; |
| neuper@42450 | 18 |
"----------- fun fetchproposedtacticOK2xml -----------------------"; |
| wneuper@59253 | 19 |
fetchproposedtacticOK2xml 11 (Rewrite ("rmult_commute", @{thm "rmult_commute"}));
|
| neuper@42450 | 20 |
(* |
| neuper@42450 | 21 |
@@@@@begin@@@@@ |
| neuper@42450 | 22 |
11 |
| neuper@42450 | 23 |
<NEXTTAC> |
| neuper@42450 | 24 |
<CALCID> 11 </CALCID> |
| neuper@42450 | 25 |
<REWRITETACTIC name="Rewrite"> |
| neuper@42450 | 26 |
<THEOREM> |
| neuper@42450 | 27 |
<ID> rmult_commute </ID> |
| neuper@42450 | 28 |
<FORMULA> |
| neuper@42450 | 29 |
<MATHML> |
| neuper@42450 | 30 |
<ISA> ?m * ?n = ?n * ?m </ISA> |
| neuper@42450 | 31 |
</MATHML> |
| neuper@42450 | 32 |
</FORMULA> |
| neuper@42450 | 33 |
</THEOREM> |
| neuper@42450 | 34 |
</REWRITETACTIC> |
| neuper@42450 | 35 |
</NEXTTAC> |
| neuper@42450 | 36 |
@@@@@end@@@@@ |
| neuper@42450 | 37 |
*) |
| neuper@42450 | 38 |
|
| neuper@42450 | 39 |
"----------- fun findFillpatterns2xml ----------------------------"; |
| neuper@42450 | 40 |
"----------- fun findFillpatterns2xml ----------------------------"; |
| neuper@42450 | 41 |
"----------- fun findFillpatterns2xml ----------------------------"; |
| walther@59997 | 42 |
findFillpatterns2xml 11 ["fill-d_d-arg", "fill-both-args"] |
| neuper@42450 | 43 |
(* |
| neuper@42450 | 44 |
@@@@@begin@@@@@ |
| neuper@42450 | 45 |
11 |
| neuper@42450 | 46 |
<FINDFILLPATTERNS> |
| neuper@42450 | 47 |
<CALCID> 11 </CALCID> |
| neuper@42450 | 48 |
<STRINGLIST> |
| neuper@42450 | 49 |
<STRING> fill-d_d-arg </STRING> |
| neuper@42450 | 50 |
<STRING> fill-both-args </STRING> |
| neuper@42450 | 51 |
</STRINGLIST> |
| neuper@42450 | 52 |
</FINDFILLPATTERNS> |
| neuper@42450 | 53 |
@@@@@end@@@@@ |
| neuper@42450 | 54 |
*) |