Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/Test_Some.thy
author Walther Neuper <neuper@ist.tugraz.at>
Mon, 02 Sep 2013 16:16:08 +0200
changeset 52101 c3f399ce32af
parent 52077 ab40ffae86a8
child 52105 2786cc9704c8
permissions -rw-r--r--
Test_Isac works again, almost ..

4 files raise errors:
# Interpret/solve.sml: "solve.sml: interSteps on norm_Rational 2"
# Interpret/inform.sml: "inform.sml: [rational,simplification] 2"
# Knowledge/partial_fractions.sml: "autoCalculate for met_partial_fraction changed: final result"
# Knowledge/eqsystem.sml: "eqsystem.sml: exp 7.70 normalize 4x4 by rewrite changed"

The chunk of changes is due to the fact, that Isac's code still is unstable.
The changes are accumulated since e8f46493af82. 
     1 theory Test_Some imports Isac

     2 begin 

     3 ML_file "Knowledge/rational.sml"

     4 

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

     6 ML {*

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

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

     9 

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

    11 

    12 *}

    13 text {*

    14   declare [[show_types]] 

    15   declare [[show_sorts]]

    16   find_theorems "?a <= ?a"

    17   

    18   print_facts

    19   print_statement ""

    20   print_theory

    21 *}

    22 ML {*

    23 (*========== inhibit exn WN130822 only runs with Rational2.thy =================================

    24 ============ inhibit exn WN130822 only runs with Rational2.thy ================================*)

    25 

    26 (*========== inhibit exn WN130826 TODO =========================================================

    27 ============ inhibit exn WN130826 TODO ========================================================*)

    28 

    29 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.

    30 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-*)

    31 

    32 (*=========================^^^ correct until here ^^^==========================================*)

    33 *}

    34 

    35 

    36 section {* ====================================================================================*}

    37 ML {*

    38 *} ML {*

    39 *} ML {*

    40 *} ML {*

    41 *} ML {*

    42 *}

    43 

    44 section {* GREAT CONFUSION -> final hg ci =====================================================*}

    45 ML {*

    46 (*in isabisac12/test/../rational.sml*)

    47 "-------- investigate rls common_nominator_p from OLD gcd --------------------";

    48 (*ATTENTION:

    49 val common_nominator_p =

    50   Rrls {id = "common_nominator_p", ...

    51 	  scr = Rfuns {init_state  = init_state thy Atools_erls ro,

    52 		  normal_form = add_fraction_p_ thy, <<<===================================

    53 :

    54 val add_fractions_p = common_nominator_p; (*FIXXXME:eilig f"ur norm_Rational*)

    55 (*but ^^^ not exported, just ^^^*)

    56 

    57 i.e. GREAT CONFUSION:

    58 # normal_form of add_fractions_p is add_fraction_p_,

    59 # and id of add_fractions_p is common_nominator_p

    60 *)

    61 

    62 section {* ===================================================================================*}

    63 ML {*

    64 *} ML {*

    65 *} ML {*

    66 *}

    67 

    68 section {* ===================================================================================*}

    69 ML {*

    70 *} ML {*

    71 *} ML {*

    72 *}

    73 end
wneuper/isa