test/Tools/isac/Test_Some.thy
branchdecompose-isar
changeset 42272 dcc5d2601cf7
parent 42255 6201b34bd323
child 42278 753c1a5fe3aa
equal deleted inserted replaced
42269:b8a255b0ba3b 42272:dcc5d2601cf7
     5         10        20        30        40        50        60        70        80
     5         10        20        30        40        50        60        70        80
     6 *)
     6 *)
     7 
     7 
     8 theory Test_Some imports Isac begin
     8 theory Test_Some imports Isac begin
     9 
     9 
    10 use"../../../test/Tools/isac/Frontend/interface.sml" 
    10 use"../../../test/Tools/isac/Knowledge/polyeq.sml" 
       
    11 
       
    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 {*
       
    20 
       
    21 *}
       
    22 ML {*
       
    23 
       
    24 *}
       
    25 ML {*
       
    26 
       
    27 *}
    11 
    28 
    12 ML {*
    29 ML {*
    13 val c = [];
    30 val c = [];
    14 print_depth 5;
    31 print_depth 5;
       
    32 *}
       
    33 ML {*
       
    34 
       
    35 *}
       
    36 ML {*
       
    37 
       
    38 *}
       
    39 ML {*
       
    40 
       
    41 *}
       
    42 ML {*
       
    43 
    15 *}
    44 *}
    16 ML {*
    45 ML {*
    17 
    46 
    18 *}
    47 *}
    19 ML{*
    48 ML{*