21 writeln "======= KEStore_Elems.get_calcs @{theory} ordered ======="; |
21 writeln "======= KEStore_Elems.get_calcs @{theory} ordered ======="; |
22 KEStore_Elems.get_calcs @{theory} |
22 KEStore_Elems.get_calcs @{theory} |
23 |> map string_of_calc |> enumerate_strings |> sort string_ord |> map writeln; |
23 |> map string_of_calc |> enumerate_strings |> sort string_ord |> map writeln; |
24 writeln "======= end KEStore_Elems.get_calcs @{theory} ======="; |
24 writeln "======= end KEStore_Elems.get_calcs @{theory} ======="; |
25 |
25 |
26 (* use a diff-tool for comparing KEStore_Elems.get_rlss <--> ! ruleset' *) |
26 (* use a diff-tool for comparing KEStore_Elems.get_rlss <--> ! xxx *) |
27 writeln "======= begin ! calclist' ======="; |
27 writeln "======= begin ! calclist' ======="; |
28 ! calclist' |> rev (*!!!!!*) |
28 ! calclist' |> rev (*!!!!!*) |
29 |> map string_of_calc |> map writeln; |
29 |> map string_of_calc |> map writeln; |
30 writeln "======= ! calclist' ordered ======="; |
30 writeln "======= ! calclist' ordered ======="; |
31 ! calclist' |> rev (*!!!!!*) |
31 ! calclist' |> rev (*!!!!!*) |
47 val knowthys' = |
47 val knowthys' = |
48 take ((find_index (curry Theory.eq_thy first_Knowledge_thy) isacthys') + 1, isacthys'); |
48 take ((find_index (curry Theory.eq_thy first_Knowledge_thy) isacthys') + 1, isacthys'); |
49 val progthys' = (*WN120321.TODO rearrange theories -------vvv*) |
49 val progthys' = (*WN120321.TODO rearrange theories -------vvv*) |
50 drop ((find_index (curry Theory.eq_thy first_Knowledge_thy) isacthys') + 1 +3, isacthys'); |
50 drop ((find_index (curry Theory.eq_thy first_Knowledge_thy) isacthys') + 1 +3, isacthys'); |
51 |
51 |
52 val isacrlsthms = (*! ruleset'*) (*SWITCH*) (KEStore_Elems.get_rlss @{theory})(**) |
52 val isacrlsthms = (KEStore_Elems.get_rlss @{theory}) |
53 |> map (thms_of_rls o #2 o #2) |
53 |> map (thms_of_rls o #2 o #2) |
54 |> flat |
54 |> flat |
55 |> map thm_of_thm |
55 |> map thm_of_thm |
56 |> gen_distinct Thm.eq_thm |
56 |> gen_distinct Thm.eq_thm |
57 |> map (` I) |
57 |> map (` I) |
281 (remarkably, "Interpret/calchead.sml" sometimes has an error, sometimes not |
281 (remarkably, "Interpret/calchead.sml" sometimes has an error, sometimes not |
282 when cutting/pasting check_unsynchronized_ref in Isabelle2011; |
282 when cutting/pasting check_unsynchronized_ref in Isabelle2011; |
283 but this is permanently without errors in Isabelle2012). |
283 but this is permanently without errors in Isabelle2012). |
284 |
284 |
285 The major cases of "Unsynchronized.ref" are those in "~~/src/Tools/isac/calcelems.sml", |
285 The major cases of "Unsynchronized.ref" are those in "~~/src/Tools/isac/calcelems.sml", |
286 thehier, ptyps, mets, theory', rew_ord', ruleset', calclist', |
286 thehier, ptyps, mets, theory', rew_ord', ruleset'-->KEStore_Elems.add_rlss\get_rlss, |
|
287 calclist', |
287 which shall be handled by "Theory_Data", see |
288 which shall be handled by "Theory_Data", see |
288 "~~/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml". |
289 "~~/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml". |
289 |
290 |
290 The transition from the above "Unsynchronized.ref" to "Theory_Data" is a task |
291 The transition from the above "Unsynchronized.ref" to "Theory_Data" is a task |
291 to be scheduled for several days. An exception is "thehier", see (1.2) (1.3) below. |
292 to be scheduled for several days. An exception is "thehier", see (1.2) (1.3) below. |