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

*}

ML {*

    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');

*}

ML {*

    val isacthms = 

              (flat o (map Theory.axioms_of)) isacthys : (thmID * term) list; 

*}

ML {*

(*in*)

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

(*end;*)

*}

ML {*

make_isab;

collect_thydata;

term2xml;

*}

ML {*

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

isab_thm_thy := make_isab rlsthmsNOTisac isabthys;

*}

ML {*

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