1.1 --- a/src/Tools/isac/Knowledge/RootRat.thy	Fri Aug 27 10:39:12 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy	Fri Aug 27 14:56:54 2010 +0200
     1.3 @@ -1,16 +1,38 @@
     1.4 -(*.(c) by Richard Lang, 2003 .*)
     1.5  (* collecting all knowledge for Root and Rational
     1.6     created by: rlang 
     1.7           date: 02.10
     1.8     changed by: rlang
     1.9     last change by: rlang
    1.10               date: 02.10.20
    1.11 +   (c) by Richard Lang, 2003
    1.12  *)
    1.13  
    1.14 -RootRat = Root + Rational +
    1.15 -(*-------------------- consts------------------------------------------------*)
    1.16 +theory RootRat imports Root Rational begin
    1.17  
    1.18 +ML {*
    1.19 +(*-------------------------rules-------------------------*)
    1.20 +val rootrat_erls = 
    1.21 +    merge_rls "rootrat_erls" Root_erls
    1.22 +     (merge_rls "" rational_erls
    1.23 +      (append_rls "" e_rls
    1.24 +		[]));
    1.25  
    1.26 -(*-------------------- rules------------------------------------------------*)
    1.27 +ruleset' := overwritelthy thy (!ruleset',
    1.28 +	     [("rootrat_erls",rootrat_erls) (*FIXXXME:del with rls.rls'*)]);
    1.29 +
    1.30 +(*.calculate numeral groundterms.*)
    1.31 +val calculate_RootRat = 
    1.32 +    append_rls "calculate_RootRat" calculate_Rational
    1.33 +	       [Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
    1.34 +		(* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *)
    1.35 +		Thm ("real_mult_1",num_str real_mult_1),
    1.36 +		(* 1 * z = z *)
    1.37 +		Thm ("sym_real_mult_minus1",num_str (real_mult_minus1 RS sym)),
    1.38 +		(* "- z1 = -1 * z1"  *)
    1.39 +		Calc ("Root.sqrt",eval_sqrt "#sqrt_")
    1.40 +		];
    1.41 +ruleset' := overwritelthy thy (!ruleset',
    1.42 +			[("calculate_RootRat",calculate_RootRat)]);
    1.43 +*}
    1.44  
    1.45  end