1.1 --- a/src/Tools/isac/IsacKnowledge/Equation.ML	Wed Aug 25 15:15:01 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,85 +0,0 @@
     1.4 -(*.(c) by Richard Lang, 2003 .*)
     1.5 -(* defines equation and univariate-equation
     1.6 -   created by: rlang 
     1.7 -         date: 02.09
     1.8 -   changed by: rlang
     1.9 -   last change by: rlang
    1.10 -             date: 02.11.29
    1.11 -*)
    1.12 -
    1.13 -(* use_thy_only"IsacKnowledge/Equation";
    1.14 -   use_thy"IsacKnowledge/Equation";
    1.15 -   use"IsacKnowledge/Equation.ML";
    1.16 -   use"Equation.ML";
    1.17 -   *)
    1.18 -
    1.19 -theory' := overwritel (!theory', [("Equation.thy",Equation.thy)]);
    1.20 -
    1.21 -val univariate_equation_prls = 
    1.22 -    append_rls "univariate_equation_prls" e_rls 
    1.23 -	       [Calc ("Tools.matches",eval_matches "")];
    1.24 -ruleset' := 
    1.25 -overwritelthy thy (!ruleset',
    1.26 -		   [("univariate_equation_prls",
    1.27 -		     prep_rls univariate_equation_prls)]);
    1.28 -
    1.29 -
    1.30 -store_pbt 
    1.31 - (prep_pbt Equation.thy "pbl_equ" [] e_pblID
    1.32 - (["equation"],
    1.33 -  [("#Given" ,["equality e_","solveFor v_"]),
    1.34 -   ("#Where" ,["matches (?a = ?b) e_"]),
    1.35 -   ("#Find"  ,["solutions v_i_"])
    1.36 -  ],
    1.37 -  append_rls "equation_prls" e_rls 
    1.38 -	     [Calc ("Tools.matches",eval_matches "")],
    1.39 -  SOME "solve (e_::bool, v_)",
    1.40 -  []));
    1.41 -
    1.42 -store_pbt
    1.43 - (prep_pbt Equation.thy "pbl_equ_univ" [] e_pblID
    1.44 - (["univariate","equation"],
    1.45 -  [("#Given" ,["equality e_","solveFor v_"]),
    1.46 -   ("#Where" ,["matches (?a = ?b) e_"]),
    1.47 -   ("#Find"  ,["solutions v_i_"])
    1.48 -  ],
    1.49 -  univariate_equation_prls,SOME "solve (e_::bool, v_)",[]));
    1.50 -
    1.51 -
    1.52 -(*.function for handling the cas-input "solve (x+1=2, x)":
    1.53 -   make a model which is already in ptree-internal format.*)
    1.54 -(* val (h,argl) = strip_comb (str2term "solve (x+1=2, x)");
    1.55 -   val (h,argl) = strip_comb ((term_of o the o (parse thy)) 
    1.56 -				  "solveTest (x+1=2, x)");
    1.57 -   *)
    1.58 -fun argl2dtss [Const ("Pair", _) $ eq $ bdv] =
    1.59 -    [((term_of o the o (parse thy)) "equality", [eq]),
    1.60 -     ((term_of o the o (parse thy)) "solveFor", [bdv]),
    1.61 -     ((term_of o the o (parse thy)) "solutions", 
    1.62 -      [(term_of o the o (parse thy)) "L"])
    1.63 -     ]
    1.64 -  | argl2dtss _ = raise error "Equation.ML: wrong argument for argl2dtss";
    1.65 -
    1.66 -castab := 
    1.67 -overwritel (!castab, 
    1.68 -	    [((term_of o the o (parse thy)) "solveTest", 
    1.69 -	      (("Test.thy", ["univariate","equation","test"], ["no_met"]), 
    1.70 -	       argl2dtss)),
    1.71 -	     ((term_of o the o (parse thy)) "solve",  
    1.72 -	      (("Isac.thy", ["univariate","equation"], ["no_met"]), 
    1.73 -	       argl2dtss))
    1.74 -	     ]);
    1.75 -
    1.76 -
    1.77 -
    1.78 -store_met
    1.79 -    (prep_met Equation.thy "met_equ" [] e_metID
    1.80 -	      (["Equation"],
    1.81 -	       [],
    1.82 -	       {rew_ord'="tless_true", rls'=Erls, calc = [], 
    1.83 -		srls = e_rls, 
    1.84 -		prls=e_rls,
    1.85 -	     crls = Atools_erls, nrls = e_rls},
    1.86 -"empty_script"
    1.87 -));
    1.88 -