(* theory collecting all knowledge defined so far

    WN.11.00

  *)

 theory Isac imports PolyMinus PolyEq Vect DiffApp Biegelinie AlgEin

        (*InsSort +*) Test begin

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

    Poly				Root

      |\__________		 |

      |		 \ 		 |

      |		Rational	 |

      |		  |		 |

    PolyEq	RatEq		RootEq

       \         /  \           /

        \       /    \         /

 	RatPolyEq    RatRootEq    etc.

 *}

 ML {*

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

 (*local*)

     val allthys = Theory.ancestors_of @{theory};            (*116*)

     val isabthys = Theory.ancestors_of first_isac_thy;      (* 86; isa02:58*)

     val isacthys = subtract Theory.eq_thy isabthys allthys; (* 30*)

     val isacrlsthms = ((map (apsnd prop_of)) o

                        (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 Theory.axioms_of)) isacthys : (thmID * term) list; 

 (*in*)

     val rlsthmsNOTisac = gen_diff eq_thmI' (isacrlsthms, isacthms); 

     (*length rlsthmsNOTisac;-->45*)

 (*end;*)

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

 isab_thm_thy := make_isab rlsthmsNOTisac isabthys;

 (*.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