1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/IsacKnowledge/Isac.ML Thu Aug 12 11:02:32 2010 +0200
1.3 @@ -0,0 +1,37 @@
1.4 +(* collect all knowledge defined in theories so far
1.5 + author: Walther Neuper 0003
1.6 + (c) isac-team
1.7 +
1.8 +use"IsacKnowledge/Isac.ML";
1.9 +use"Isac.ML";
1.10 + *)
1.11 +
1.12 +
1.13 +theory' := overwritel (!theory', [("Isac.thy",Isac.thy)]);
1.14 +
1.15 +
1.16 +(**.set up a list for getting guh + theID for a thm (defined in isabelle).**)
1.17 +
1.18 +(*.get all theorems used by isac and defined in isabelle.*)
1.19 +local
1.20 + val isacrlsthms = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o
1.21 + (map (thms_of_rls o #2 o #2))) (!ruleset');
1.22 + val isacthms = (flat o (map (thms_of o #2))) (!theory');
1.23 +in
1.24 + val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms);
1.25 +end;
1.26 +
1.27 +(*.set up the list using 'val first_isac_thy' (see ListG.ML).*)
1.28 +isab_thm_thy := make_isab rlsthmsNOTisac
1.29 + ((#ancestors o rep_theory) first_isac_thy);
1.30 +
1.31 +
1.32 +(*.create the hierarchy of theory elements from IsacKnowledge
1.33 + including thms from Isabelle used in rls;
1.34 + elements store_*d in any *.ML are not overwritten.*)
1.35 +
1.36 +thehier := the_hier (!thehier) (collect_thydata ());
1.37 +writeln("----------------------------------\n\
1.38 + \*** insert: not found ... IS OK : \n\
1.39 + \comes from fill_parents \n\
1.40 + \----------------------------------\n");