(*.(c) by Richard Lang, 2003 .*)

 (* collecting all knowledge for Root and Rational

    created by: rlang 

          date: 02.10

    changed by: rlang

    last change by: rlang

              date: 02.10.21

 *)

 (* use"knowledge/RootRat.ML";

    use"RootRat.ML";

    use"ROOT.ML";

    cd"knowledge";

    remove_thy"RootRat";

    use_thy"Isac";

    *)

 "******* RootRat.ML begin *******";

 theory' := overwritel (!theory', [("RootRat.thy",RootRat.thy)]);

 (*-------------------------functions---------------------*)

 (*-------------------------rulse-------------------------*)

 val rootrat_erls = 

     merge_rls "rootrat_erls" Root_erls

      (merge_rls "" rational_erls

       (append_rls "" e_rls

 		[]));

 ruleset' := overwritelthy thy (!ruleset',

 			[("rootrat_erls",rootrat_erls) (*FIXXXME:del with rls.rls'*) 

 			 ]);

 (*.calculate numeral groundterms.*)

 val calculate_RootRat = 

     append_rls "calculate_RootRat" calculate_Rational

 	       [Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),

 		(* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *)

 		Thm ("real_mult_1",num_str real_mult_1),

 		(* 1 * z = z *)

 		Thm ("sym_real_mult_minus1",num_str (real_mult_minus1 RS sym)),

 		(* "- z1 = -1 * z1"  *)

 		Calc ("Root.sqrt",eval_sqrt "#sqrt_")

 		];

 ruleset' := overwritelthy thy (!ruleset',

 			[("calculate_RootRat",calculate_RootRat)]);

 "******* RootRat.ML end *******";