1 (* Title: Run_Tests as long Isac is not available: REPLACE 'IMPORTS'
2 Author: Walther Neuper 101001
3 (c) copyright due to lincense terms.
5 $ cd /usr/local/isabisac/test/Tools/isac
6 $ /usr/local/isabisac/bin/isabelle emacs Test_Some.thy &
9 theory Test_Isac imports "Knowledge/Rational" begin
10 (*..................................########..................................*)
12 ML{* writeln "**** run the test ***************************************" *};
15 fun term2st t = Print_Mode.setmp [] (Syntax.string_of_term
16 (ProofContext.init_global (Thy_Info.get_Thy_Info.get_theory "Rational"))) t;
17 (*..............................................########......................*)
20 use"../../../test/Tools/isac/Knowledge/polyminus.sml";