1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/Knowledge/Isac.ML	Wed Aug 25 16:20:07 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"Knowledge/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 (PureThy.all_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 ListC.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");