1 (* collect all knowledge defined in theories so far
2 author: Walther Neuper 0003
5 use"Knowledge/Isac.ML";
10 theory' := overwritel (!theory', [("Isac.thy",Isac.thy)]);
13 (**.set up a list for getting guh + theID for a thm (defined in isabelle).**)
15 (*.get all theorems used by isac and defined in isabelle.*)
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 (PureThy.all_thms_of o #2))) (!theory');
21 val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms);
24 (*.set up the list using 'val first_isac_thy' (see ListC.ML).*)
25 isab_thm_thy := make_isab rlsthmsNOTisac
26 ((#ancestors o rep_theory) first_isac_thy);
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.*)
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");