1.1 --- a/test/Tools/isac/Test_Some.thy Mon Sep 16 11:28:43 2013 +0200
1.2 +++ b/test/Tools/isac/Test_Some.thy Mon Sep 16 12:20:00 2013 +0200
1.3 @@ -20,54 +20,32 @@
1.4 print_theory
1.5 *}
1.6 ML {*
1.7 -(*========== inhibit exn WN130822 only runs with Rational2.thy =================================
1.8 -============ inhibit exn WN130822 only runs with Rational2.thy ================================*)
1.9 -
1.10 -(*========== inhibit exn WN130826 TODO =========================================================
1.11 -============ inhibit exn WN130826 TODO ========================================================*)
1.12 -
1.13 +(*========== inhibit exn WN130909 TODO =========================================================
1.14 +============ inhibit exn WN130909 TODO ========================================================*)
1.15 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
1.16 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-*)
1.17 -
1.18 -(*=========================^^^ correct until here ^^^==========================================*)
1.19 *}
1.20
1.21 -
1.22 -section {* ====================================================================================*}
1.23 -ML {*
1.24 -*} ML {*
1.25 -*} ML {*
1.26 -*} ML {*
1.27 -*} ML {*
1.28 -*}
1.29 -
1.30 -section {* GREAT CONFUSION -> final hg ci =====================================================*}
1.31 -ML {*
1.32 -(*in isabisac12/test/../rational.sml*)
1.33 -"-------- investigate rls common_nominator_p from OLD gcd --------------------";
1.34 -(*ATTENTION:
1.35 -val common_nominator_p =
1.36 - Rrls {id = "common_nominator_p", ...
1.37 - scr = Rfuns {init_state = init_state thy Atools_erls ro,
1.38 - normal_form = add_fraction_p_ thy, <<<===================================
1.39 -:
1.40 -val add_fractions_p = common_nominator_p; (*FIXXXME:eilig f"ur norm_Rational*)
1.41 -(*but ^^^ not exported, just ^^^*)
1.42 -
1.43 -i.e. GREAT CONFUSION:
1.44 -# normal_form of add_fractions_p is add_fraction_p_,
1.45 -# and id of add_fractions_p is common_nominator_p
1.46 -*)
1.47 -
1.48 section {* ===================================================================================*}
1.49 ML {*
1.50 *} ML {*
1.51 *} ML {*
1.52 +*} ML {*
1.53 +*}
1.54 +
1.55 +
1.56 +section {* ===================================================================================*}
1.57 +ML {*
1.58 +*} ML {*
1.59 +*} ML {*
1.60 +*} ML {*
1.61 *}
1.62
1.63 section {* ===================================================================================*}
1.64 ML {*
1.65 *} ML {*
1.66 *} ML {*
1.67 +*} ML {*
1.68 *}
1.69 +
1.70 end