(* Title:  collecting all knowledge for Root and Rational

    Author: Richard Lang 02.10 last change by: rlang date: 02.10.20

    (c) due to copyright terms

 *)

 theory RootRat imports Root Rational begin

 ML {*

 val thy = @{theory};

 val rootrat_erls = 

   merge_rls "rootrat_erls" Root_erls

     (merge_rls "" rational_erls

       (append_rls "" e_rls []));

 (*.calculate numeral groundterms.*)

 val calculate_RootRat = 

   append_rls "calculate_RootRat" calculate_Rational

 	    [Thm ("distrib_left",num_str @{thm distrib_left}),

 		      (* 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 ("NthRoot.sqrt",eval_sqrt "#sqrt_")

 		     ];

 *}

 setup {* KEStore_Elems.add_rlss 

   [("rootrat_erls", (Context.theory_name @{theory}, prep_rls rootrat_erls)), 

   ("calculate_RootRat", (Context.theory_name @{theory}, prep_rls calculate_RootRat))] *}

 end