1.1 --- a/src/Tools/isac/IsacKnowledge/RootRat.ML	Wed Aug 25 15:15:01 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,50 +0,0 @@
     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 *******";