wneuper/isa: test/Tools/isac/Test

     1 (* Title:  run tests on a particular test file

     2    Author: Walther Neuper 101001

     3    (c) copyright due to lincense terms.

     4 12345678901234567890123456789012345678901234567890123456789012345678901234567890

     5         10        20        30        40        50        60        70        80

     6 *)

     8 theory Test_Some imports Isac begin

    10 use"../../../test/Tools/isac/Knowledge/polyeq.sml"

    12 ML {*

    13 (*GOON: polyeq first ML, test 1 above, and the all below piecewiese*)

    14 *}

    15 ML {*

    16 val t = @{term "(2::real)*r*2.14"};

    17 term2str t;

    18 *}

    19 ML {*

    21 *}

    22 ML {*

    24 *}

    25 ML {*

    27 *}

    29 ML {*

    30 val c = [];

    31 print_depth 5;

    32 *}

    33 ML {*

    35 *}

    36 ML {*

    38 *}

    39 ML {*

    41 *}

    42 ML {*

    44 *}

    45 ML {*

    47 *}

    48 ML{*

    49 *}

    50 ML{*

    51 *}

    52 ML {* (*=================*)

    53 *}

    54 ML{*

    55 "~~~~~ fun , args:"; val () = ();

    56 *}

    57 end

    60 (*============ inhibit exn WN110906 ==============================================

    61 ============ inhibit exn WN110906 ==============================================*)

    64 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.

    65 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)

author	Walther Neuper <neuper@ist.tugraz.at>
	Sun, 18 Sep 2011 15:21:46 +0200
branch	decompose-isar
changeset 42272	dcc5d2601cf7
parent 42255	6201b34bd323
child 42278	753c1a5fe3aa
permissions	-rw-r--r--