wneuper/isa: test/Tools/isac/Test_Theory.thy@cd5494eb08fd

     1 theory Test_Theory imports "~~/src/Tools/isac/Knowledge/Rational"

     2 begin

     3 ML_file "~~/src/Tools/isac/ProgLang/scrtools.sml"

     4 (* ATTENTION: tests with CalcTreeTest, CalcTree do NOT work here, because Thy_Info.get_theory

     5   requires session Isac, see ~~/test/Tools/isac/ADDTESTS/session-get_theory *)

     7 section {* code for copy & paste ===============================================================*}

     8 ML {*

     9 "~~~~~ fun , args:"; val () = ();

    10 "~~~~~ and , args:"; val () = ();

    12 "~~~~~ to  return val:"; val () = ();

    14 *}

    15 text {*

    16   declare [[show_types]]

    17   declare [[show_sorts]]

    18   find_theorems "?a <= ?a"

    20   print_facts

    21   print_statement ""

    22   print_theory

    23 *}

    24 ML {*

    25 (*========== inhibit exn WN130909 TODO =========================================================

    26 ============ inhibit exn WN130909 TODO ========================================================*)

    27 (*-.-.-.-.-. isolate response ad-hoc .-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.

    28 -.-.-.-.-.-. isolate response ad-hoc .-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-*)

    29 *}

    31 section {* =================================================================*}

    32 ML {*

    33 *} ML {*

    34 *} ML {*

    35 *} ML {*

    36 *} ML {*

    37 *} ML {*

    38 *} ML {*

    39 *}

    40 section {* =================================================================*}

    41 ML {*

    42 *} ML {*

    43 *} ML {*

    44 *} ML {*

    45 *} ML {*

    46 *} ML {*

    47 *} ML {*

    48 *} ML {*

    49 *}

    50 section {* =================================================================*}

    51 ML {*

    52 *} ML {*

    53 *} ML {*

    54 *} ML {*

    55 *} ML {*

    56 *} ML {*

    57 *} ML {*

    58 *} ML {*

    59 *}

    61 end

author	Walther Neuper <neuper@ist.tugraz.at>
	Fri, 13 Sep 2013 18:57:11 +0200
changeset 52102	cd5494eb08fd
child 52146	f47e195af9a3
permissions	-rw-r--r--