author | Thomas Leh <t.leh@gmx.at> |
Tue, 19 Jul 2011 13:04:59 +0200 | |
branch | decompose-isar |
changeset 42115 | 41a68869d217 |
parent 42114 | d301c7a68bba |
child 42116 | 536a9fb832c1 |
permissions | -rw-r--r-- |
neuper@41982 | 1 |
(* Title: run tests on a particular test file |
neuper@41943 | 2 |
Author: Walther Neuper 101001 |
neuper@41943 | 3 |
(c) copyright due to lincense terms. |
neuper@41943 | 4 |
*) |
neuper@41943 | 5 |
|
neuper@41943 | 6 |
theory Test_Some imports Isac begin |
neuper@41943 | 7 |
|
akargl@42108 | 8 |
ML{* writeln "**** run the test ***************************************" *} |
akargl@42108 | 9 |
|
t@42115 | 10 |
use"../../../test/Tools/isac/Knowledge/integrate.sml" |
akargl@42108 | 11 |
|
t@42098 | 12 |
ML{* |
t@42111 | 13 |
|
akargl@42110 | 14 |
|
t@42098 | 15 |
*} |
neuper@41943 | 16 |
|
t@42115 | 17 |
ML{* |
t@42115 | 18 |
|
t@42115 | 19 |
*} |
t@42115 | 20 |
ML{* |
t@42115 | 21 |
p |
t@42115 | 22 |
*} |
t@42115 | 23 |
ML{* |
t@42115 | 24 |
|
t@42115 | 25 |
*} |
neuper@41943 | 26 |
end |
neuper@41943 | 27 |
|
neuper@41943 | 28 |
|
neuper@41943 | 29 |
(*=== inhibit exn ?============================================================= |
neuper@41943 | 30 |
===== inhibit exn ?===========================================================*) |
neuper@41943 | 31 |
|
neuper@41943 | 32 |
|
neuper@42107 | 33 |
(*========== inhibit exn 110719 ================================================ |
neuper@42107 | 34 |
============ inhibit exn 110719 ==============================================*) |
neuper@41943 | 35 |
|
neuper@41943 | 36 |
|
neuper@41943 | 37 |
(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. |
neuper@41943 | 38 |
-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) |