18 print_facts |
18 print_facts |
19 print_statement "" |
19 print_statement "" |
20 print_theory |
20 print_theory |
21 *} |
21 *} |
22 ML {* |
22 ML {* |
23 (*========== inhibit exn WN130822 only runs with Rational2.thy ================================= |
23 (*========== inhibit exn WN130909 TODO ========================================================= |
24 ============ inhibit exn WN130822 only runs with Rational2.thy ================================*) |
24 ============ inhibit exn WN130909 TODO ========================================================*) |
25 |
|
26 (*========== inhibit exn WN130826 TODO ========================================================= |
|
27 ============ inhibit exn WN130826 TODO ========================================================*) |
|
28 |
|
29 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. |
25 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. |
30 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-*) |
26 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-*) |
31 |
|
32 (*=========================^^^ correct until here ^^^==========================================*) |
|
33 *} |
27 *} |
34 |
28 |
35 |
29 section {* ===================================================================================*} |
36 section {* ====================================================================================*} |
|
37 ML {* |
30 ML {* |
38 *} ML {* |
31 *} ML {* |
39 *} ML {* |
32 *} ML {* |
40 *} ML {* |
33 *} ML {* |
41 *} ML {* |
34 *} |
42 *} |
|
43 |
35 |
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 |
36 |
62 section {* ===================================================================================*} |
37 section {* ===================================================================================*} |
63 ML {* |
38 ML {* |
|
39 *} ML {* |
64 *} ML {* |
40 *} ML {* |
65 *} ML {* |
41 *} ML {* |
66 *} |
42 *} |
67 |
43 |
68 section {* ===================================================================================*} |
44 section {* ===================================================================================*} |
69 ML {* |
45 ML {* |
70 *} ML {* |
46 *} ML {* |
71 *} ML {* |
47 *} ML {* |
|
48 *} ML {* |
72 *} |
49 *} |
|
50 |
73 end |
51 end |