1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/test/Tools/isac/Test_Theory.thy Fri Sep 13 18:57:11 2013 +0200
1.3 @@ -0,0 +1,63 @@
1.4 +theory Test_Theory imports "~~/src/Tools/isac/Knowledge/Rational"
1.5 +begin
1.6 +ML_file "~~/src/Tools/isac/ProgLang/scrtools.sml"
1.7 +(* ATTENTION: tests with CalcTreeTest, CalcTree do NOT work here, because Thy_Info.get_theory
1.8 + requires session Isac, see ~~/test/Tools/isac/ADDTESTS/session-get_theory *)
1.9 +
1.10 +section {* code for copy & paste ===============================================================*}
1.11 +ML {*
1.12 +"~~~~~ fun , args:"; val () = ();
1.13 +"~~~~~ and , args:"; val () = ();
1.14 +
1.15 +"~~~~~ to return val:"; val () = ();
1.16 +
1.17 +*}
1.18 +text {*
1.19 + declare [[show_types]]
1.20 + declare [[show_sorts]]
1.21 + find_theorems "?a <= ?a"
1.22 +
1.23 + print_facts
1.24 + print_statement ""
1.25 + print_theory
1.26 +*}
1.27 +ML {*
1.28 +(*========== inhibit exn WN130909 TODO =========================================================
1.29 +============ inhibit exn WN130909 TODO ========================================================*)
1.30 +(*-.-.-.-.-. isolate response ad-hoc .-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
1.31 +-.-.-.-.-.-. isolate response ad-hoc .-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-*)
1.32 +*}
1.33 +
1.34 +section {* =================================================================*}
1.35 +ML {*
1.36 +*} ML {*
1.37 +*} ML {*
1.38 +*} ML {*
1.39 +*} ML {*
1.40 +*} ML {*
1.41 +*} ML {*
1.42 +*}
1.43 +section {* =================================================================*}
1.44 +ML {*
1.45 +*} ML {*
1.46 +*} ML {*
1.47 +*} ML {*
1.48 +*} ML {*
1.49 +*} ML {*
1.50 +*} ML {*
1.51 +*} ML {*
1.52 +*}
1.53 +section {* =================================================================*}
1.54 +ML {*
1.55 +*} ML {*
1.56 +*} ML {*
1.57 +*} ML {*
1.58 +*} ML {*
1.59 +*} ML {*
1.60 +*} ML {*
1.61 +*} ML {*
1.62 +*}
1.63 +
1.64 +end
1.65 +
1.66 +