Isac = PolyMinus + PolyEq + Vect + DiffApp + Biegelinie + AlgEin

 theory Isac imports PolyMinus PolyEq Vect DiffApp Biegelinie AlgEin

        + (*InsSort +*) Test + 

        (*InsSort +*) Test begin

 end

 text {* dependencies alternative to those defined by R.Lang during his thesis:

 (* dependencies alternative to those defined by R.Lang during his thesis:

 *)

 *}

 ML {*

 (**.set up a list for getting guh + theID for a thm (defined in isabelle).**)

 (*.get all theorems used by isac and defined in isabelle.*)

 local

     val isacrlsthms = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o 

 		       (map (thms_of_rls o #2 o #2))) (!ruleset');

     val isacthms = (flat o (map (PureThy.all_thms_of o #2))) 

                        (*WN100827 TODOOOOO*)(!theory');

 in

     val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms);

 end;

 (*.set up the list using 'val first_isac_thy' (see ListC.ML).*)

 isab_thm_thy := make_isab rlsthmsNOTisac

 			  ((#ancestors o rep_theory) first_isac_thy);

 (*.create the hierarchy of theory elements from IsacKnowledge

    including thms from Isabelle used in rls;

    elements store_*d in any *.ML are not overwritten.*)

 thehier := the_hier (!thehier) (collect_thydata ());

 writeln("----------------------------------\n" ^

 	"*** insert: not found ... IS OK : \n" ^

 	"comes from fill_parents           \n" ^

 	"----------------------------------\n");

 *}

 end