49 drop ((find_index (curry Context.eq_thy @{theory Complex_Main}) allthys), allthys); |
49 drop ((find_index (curry Context.eq_thy @{theory Complex_Main}) allthys), allthys); |
50 val isacthys' = (*["Isac", "Inverse_Z_Transform", .., "KEStore"]*) |
50 val isacthys' = (*["Isac", "Inverse_Z_Transform", .., "KEStore"]*) |
51 take ((find_index (curry Context.eq_thy @{theory Complex_Main}) allthys), allthys); |
51 take ((find_index (curry Context.eq_thy @{theory Complex_Main}) allthys), allthys); |
52 val knowthys' = (*["Isac", .., "Descript", "Delete"]*) |
52 val knowthys' = (*["Isac", .., "Descript", "Delete"]*) |
53 take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys'); |
53 take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys'); |
54 val progthys' = (*["Script", "Tools", "ListC", "KEStore"]*) |
54 val progthys' = (*["Program", "Tools", "ListC", "KEStore"]*) |
55 drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys'); |
55 drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys'); |
56 val isacrlsthms = (*length = 460*) |
56 val isacrlsthms = (*length = 460*) |
57 thms_of_rlss @{theory} (KEStore_Elems.get_rlss knowledge_parent) : (thmID * thm) list |
57 thms_of_rlss @{theory} (KEStore_Elems.get_rlss knowledge_parent) : (thmID * thm) list |
58 val rlsthmsNOTisac = isacrlsthms (*length = 36*) |
58 val rlsthmsNOTisac = isacrlsthms (*length = 36*) |
59 |> filter (fn (deriv, _) => |
59 |> filter (fn (deriv, _) => |