1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/Knowledge/RootRat.ML	Wed Aug 25 16:20:07 2010 +0200
     1.3 @@ -0,0 +1,50 @@
     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.21
    1.11 +*)
    1.12 +(* use"knowledge/RootRat.ML";
    1.13 +   use"RootRat.ML";
    1.14 +
    1.15 +   use"ROOT.ML";
    1.16 +   cd"knowledge";
    1.17 +
    1.18 +   remove_thy"RootRat";
    1.19 +   use_thy"Isac";
    1.20 +   *)
    1.21 +
    1.22 +"******* RootRat.ML begin *******";
    1.23 +theory' := overwritel (!theory', [("RootRat.thy",RootRat.thy)]);
    1.24 +
    1.25 +(*-------------------------functions---------------------*)
    1.26 +
    1.27 +(*-------------------------rulse-------------------------*)
    1.28 +val rootrat_erls = 
    1.29 +    merge_rls "rootrat_erls" Root_erls
    1.30 +     (merge_rls "" rational_erls
    1.31 +      (append_rls "" e_rls
    1.32 +		[]));
    1.33 +
    1.34 +ruleset' := overwritelthy thy (!ruleset',
    1.35 +			[("rootrat_erls",rootrat_erls) (*FIXXXME:del with rls.rls'*) 
    1.36 +			 ]);
    1.37 +
    1.38 +(*.calculate numeral groundterms.*)
    1.39 +val calculate_RootRat = 
    1.40 +    append_rls "calculate_RootRat" calculate_Rational
    1.41 +	       [Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
    1.42 +		(* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *)
    1.43 +		Thm ("real_mult_1",num_str real_mult_1),
    1.44 +		(* 1 * z = z *)
    1.45 +		Thm ("sym_real_mult_minus1",num_str (real_mult_minus1 RS sym)),
    1.46 +		(* "- z1 = -1 * z1"  *)
    1.47 +		Calc ("Root.sqrt",eval_sqrt "#sqrt_")
    1.48 +		];
    1.49 +ruleset' := overwritelthy thy (!ruleset',
    1.50 +			[("calculate_RootRat",calculate_RootRat)]);
    1.51 +
    1.52 +
    1.53 +"******* RootRat.ML end *******";