1 |
|
2 theory Test_Some imports Isac |
1 theory Test_Some imports Isac |
3 begin ML_file "Knowledge/gcd_poly_ml.sml" |
2 begin |
4 (* |
3 ML_file "Knowledge/rational.sml" |
5 declare [[show_types]] |
|
6 declare [[show_sorts]] |
|
7 find_theorems "?a <= ?a" |
|
8 |
4 |
9 print_facts |
5 section {* code for copy & paste ===============================================================*} |
10 print_statement "" |
|
11 print_theory |
|
12 *) |
|
13 ML {* |
6 ML {* |
14 *} |
|
15 ML {* (*==================*) |
|
16 *} |
|
17 ML {* |
|
18 *} |
|
19 ML {* |
|
20 *} |
|
21 ML {* (*==================*) |
|
22 *} |
|
23 ML {* |
|
24 *} |
|
25 ML {* |
|
26 *} |
|
27 ML {* (*==================*) |
|
28 "~~~~~ fun , args:"; val () = (); |
7 "~~~~~ fun , args:"; val () = (); |
|
8 "~~~~~ and , args:"; val () = (); |
29 |
9 |
30 "~~~~~ to return val:"; val () = (); |
10 "~~~~~ to return val:"; val () = (); |
31 |
11 |
32 *} |
12 *} |
33 end |
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 ================================*) |
34 |
25 |
35 (*========== inhibit exn WN1130701 broken already in 2009-2 ======================= |
26 (*========== inhibit exn WN130826 TODO ========================================================= |
36 ============ inhibit exn WN1130701 broken already in 2009-2 =====================*) |
27 ============ inhibit exn WN130826 TODO ========================================================*) |
37 (*========== inhibit exn WN1130722 Isabelle2012-->13 thehier? works in Test_Some=== |
|
38 ============ inhibit exn WN1130722 Isabelle2012-->13 thehier? works in Test_Some=*) |
|
39 |
28 |
40 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. |
29 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. |
41 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) |
30 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-*) |
42 |
31 |
43 (*=========================^^^ correct until here ^^^===========================*) |
32 (*=========================^^^ correct until here ^^^==========================================*) |
|
33 *} |
44 |
34 |
45 |
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 |