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