| author | Walther Neuper <neuper@ist.tugraz.at> |
| Tue, 28 Sep 2010 09:06:56 +0200 | |
| branch | isac-update-Isa09-2 |
| changeset 38031 | 460c24a6a6ba |
| parent 37960 | ec20007095f2 |
| child 42145 | 43e7e9f835b1 |
| permissions | -rw-r--r-- |
| neuper@37906 | 1 |
(* tests on Tools |
| neuper@37906 | 2 |
author: Walther Neuper |
| neuper@37906 | 3 |
WN071229, |
| neuper@37906 | 4 |
(c) due to copyright terms |
| neuper@37906 | 5 |
|
| neuper@37906 | 6 |
use"../smltest/Scripts/tools.sml"; |
| neuper@37906 | 7 |
use"tools.sml"; |
| neuper@37906 | 8 |
*) |
| neuper@37906 | 9 |
val thy = Real.thy; |
| neuper@37906 | 10 |
|
| neuper@37906 | 11 |
"-----------------------------------------------------------------"; |
| neuper@37906 | 12 |
"table of contents -----------------------------------------------"; |
| neuper@37906 | 13 |
"-----------------------------------------------------------------"; |
| neuper@37906 | 14 |
"----------- fun matchsub ----------------------------------------"; |
| neuper@37906 | 15 |
"-----------------------------------------------------------------"; |
| neuper@37906 | 16 |
"-----------------------------------------------------------------"; |
| neuper@37906 | 17 |
"-----------------------------------------------------------------"; |
| neuper@37906 | 18 |
|
| neuper@37906 | 19 |
|
| neuper@37906 | 20 |
"----------- fun matchsub ----------------------------------------"; |
| neuper@37906 | 21 |
"----------- fun matchsub ----------------------------------------"; |
| neuper@37906 | 22 |
"----------- fun matchsub ----------------------------------------"; |
| neuper@37906 | 23 |
if matchsub thy (str2term "(a + (b + c))") (str2term "?x + (?y + ?z)") |
| neuper@38031 | 24 |
then () else error "tools.sml matchsub a + (b + c)"; |
| neuper@37906 | 25 |
|
| neuper@37906 | 26 |
if matchsub thy (str2term "(a + (b + c)) + d") (str2term "?x + (?y + ?z)") |
| neuper@38031 | 27 |
then () else error "tools.sml matchsub (a + (b + c)) + d"; |