| author | Thomas Leh <t.leh@gmx.at> |
| Tue, 26 Jul 2011 13:27:59 +0200 | |
| branch | decompose-isar |
| changeset 42197 | 7497ff20f1e8 |
| parent 42196 | f5f726ef4f6a |
| child 42198 | 1dc434befe11 |
| 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@42197 | 10 |
use"../../../test/Tools/isac/Knowledge/eqsystem.sml" |
| neuper@42142 | 11 |
|
| t@42098 | 12 |
ML{*
|
| t@42197 | 13 |
order_system |
| akargl@42145 | 14 |
|
| neuper@42141 | 15 |
*} |
| neuper@42141 | 16 |
ML{*
|
| akargl@42131 | 17 |
*} |
| akargl@42131 | 18 |
ML{*
|
| akargl@42145 | 19 |
*} |
| akargl@42145 | 20 |
ML{*
|
| neuper@42129 | 21 |
*} |
| neuper@42129 | 22 |
ML{*
|
| neuper@42129 | 23 |
*} |
| neuper@42129 | 24 |
ML{*
|
| neuper@42129 | 25 |
"~~~~~ fun , args:"; val () = (); |
| t@42115 | 26 |
*} |
| neuper@41943 | 27 |
end |
| neuper@41943 | 28 |
|
| neuper@41943 | 29 |
|
| neuper@42142 | 30 |
(*========== inhibit exn 110719 ================================================ |
| neuper@42142 | 31 |
============ inhibit exn 110719 ==============================================*) |
| neuper@41943 | 32 |
|
| neuper@41943 | 33 |
|
| neuper@41943 | 34 |
(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. |
| neuper@41943 | 35 |
-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) |
| neuper@42141 | 36 |