equal
deleted
inserted
replaced
|
1 (* collect all knowledge defined in theories so far |
|
2 author: Walther Neuper 0003 |
|
3 (c) isac-team |
|
4 |
|
5 use"IsacKnowledge/Isac.ML"; |
|
6 use"Isac.ML"; |
|
7 *) |
|
8 |
|
9 |
|
10 theory' := overwritel (!theory', [("Isac.thy",Isac.thy)]); |
|
11 |
|
12 |
|
13 (**.set up a list for getting guh + theID for a thm (defined in isabelle).**) |
|
14 |
|
15 (*.get all theorems used by isac and defined in isabelle.*) |
|
16 local |
|
17 val isacrlsthms = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o |
|
18 (map (thms_of_rls o #2 o #2))) (!ruleset'); |
|
19 val isacthms = (flat o (map (thms_of o #2))) (!theory'); |
|
20 in |
|
21 val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms); |
|
22 end; |
|
23 |
|
24 (*.set up the list using 'val first_isac_thy' (see ListG.ML).*) |
|
25 isab_thm_thy := make_isab rlsthmsNOTisac |
|
26 ((#ancestors o rep_theory) first_isac_thy); |
|
27 |
|
28 |
|
29 (*.create the hierarchy of theory elements from IsacKnowledge |
|
30 including thms from Isabelle used in rls; |
|
31 elements store_*d in any *.ML are not overwritten.*) |
|
32 |
|
33 thehier := the_hier (!thehier) (collect_thydata ()); |
|
34 writeln("----------------------------------\n\ |
|
35 \*** insert: not found ... IS OK : \n\ |
|
36 \comes from fill_parents \n\ |
|
37 \----------------------------------\n"); |