wneuper/isa: test/Tools/isac/Test

     1 theory Test_Some imports Isac

     2 begin

     3 ML_file "Knowledge/rational.sml"

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

     6 ML {*

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

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

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

    12 *}

    13 text {*

    14   declare [[show_types]]

    15   declare [[show_sorts]]

    16   find_theorems "?a <= ?a"

    18   print_facts

    19   print_statement ""

    20   print_theory

    21 *}

    22 ML {*

    23 (*========== inhibit exn WN130909 TODO =========================================================

    24 ============ inhibit exn WN130909 TODO ========================================================*)

    25 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.

    26 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-*)

    27 *}

    29 section {* ===================================================================================*}

    30 ML {*

    31 *} ML {*

    32 *} ML {*

    33 *} ML {*

    34 *}

    37 section {* ===================================================================================*}

    38 ML {*

    39 *} ML {*

    40 *} ML {*

    41 *} ML {*

    42 *}

    44 section {* ===================================================================================*}

    45 ML {*

    46 *} ML {*

    47 *} ML {*

    48 *} ML {*

    49 *}

    51 end

author	Walther Neuper <neuper@ist.tugraz.at>
	Mon, 16 Sep 2013 12:20:00 +0200
changeset 52105	2786cc9704c8
parent 52101	c3f399ce32af
child 52146	f47e195af9a3
permissions	-rw-r--r--