test/Tools/isac/Test_Theory.thy
changeset 52102 cd5494eb08fd
child 52146 f47e195af9a3
     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 +