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 +