(* collecting all knowledge for Root and Rational

    created by: rlang 

          date: 02.10

    changed by: rlang

    last change by: rlang

              date: 02.10.20

    (c) by Richard Lang, 2003

 *)

 theory RootRat imports Root Rational begin

 ML {*

 val thy = @{theory};

 (*-------------------------rules-------------------------*)

 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 ("right_distrib",num_str @{thm right_distrib}),

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

 		Thm ("mult_1_left",num_str @{thm mult_1_left}),

 		(* 1 * z = z *)

 		Thm ("sym_real_mult_minus1",

                       num_str (@{thm real_mult_minus1} RS @{thm sym})),

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

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

 		];

 ruleset' := overwritelthy thy (!ruleset',

 			[("calculate_RootRat",calculate_RootRat)]);

 *}

 end