test/Tools/isac/Test_Some.thy
changeset 42398 04d3f0133827
parent 42396 7dda01b5c12f
child 42399 c5bb245afb58
     1.1 --- a/test/Tools/isac/Test_Some.thy	Sat Mar 17 13:43:24 2012 +0100
     1.2 +++ b/test/Tools/isac/Test_Some.thy	Mon Mar 19 09:48:03 2012 +0100
     1.3 @@ -1,16 +1,16 @@
     1.4   
     1.5  theory Test_Some imports Isac begin
     1.6  
     1.7 -use"../../../test/Tools/isac/Knowledge/atools.sml"
     1.8 +use"../../../test/Tools/isac/Knowledge/rootrateq.sml"
     1.9  
    1.10  ML {*
    1.11 -val thy = @{theory "Atools"};
    1.12 +val thy = @{theory "RootRatEq"};
    1.13  val ctxt = ProofContext.init_global thy;
    1.14 -print_depth 999;
    1.15 +print_depth 555;
    1.16  *}
    1.17  ML {*
    1.18 -
    1.19 -
    1.20 +*}
    1.21 +ML {* (*==================*)
    1.22  *}
    1.23  ML {*
    1.24  *}
    1.25 @@ -29,6 +29,11 @@
    1.26  ML {*
    1.27  "~~~~~ fun , args:"; val () = ();
    1.28  "~~~~~ to  return val:"; val () = ();
    1.29 +
    1.30 +*}
    1.31 +text {**}
    1.32 +ML {*
    1.33 +
    1.34  *}
    1.35  end
    1.36  
    1.37 @@ -40,3 +45,4 @@
    1.38  
    1.39  (*=========================^^^ correct until here ^^^===========================*)
    1.40  
    1.41 +