author | Walther Neuper <wneuper@ist.tugraz.at> |
Thu, 20 Oct 2016 10:26:29 +0200 | |
changeset 59253 | f0bb15a046ae |
parent 59252 | 7d3dbc1171ff |
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 ----------------------------"; |
neuper@42450 | 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 |
*) |