1.1 --- a/src/Tools/isac/Knowledge/Equation.thy	Sun Mar 25 13:59:57 2018 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Equation.thy	Mon Mar 26 07:28:39 2018 +0200
     1.3 @@ -39,11 +39,11 @@
     1.4  
     1.5  ML {*
     1.6  val thy = @{theory};
     1.7 -val ctxt = Celem.thy2ctxt thy;
     1.8 +val ctxt = Rule.thy2ctxt thy;
     1.9  
    1.10  val univariate_equation_prls = 
    1.11 -    Celem.append_rls "univariate_equation_prls" Celem.e_rls 
    1.12 -	       [Celem.Calc ("Tools.matches",eval_matches "")];
    1.13 +    Rule.append_rls "univariate_equation_prls" Rule.e_rls 
    1.14 +	       [Rule.Calc ("Tools.matches",eval_matches "")];
    1.15  *}
    1.16  setup {* KEStore_Elems.add_rlss [("univariate_equation_prls",
    1.17    (Context.theory_name @{theory}, LTool.prep_rls @{theory} univariate_equation_prls))] *}
    1.18 @@ -53,7 +53,7 @@
    1.19          [("#Given" ,["equality e_e","solveFor v_v"]),
    1.20            ("#Where" ,["matches (?a = ?b) e_e"]),
    1.21            ("#Find"  ,["solutions v_v'i'"])],
    1.22 -        Celem.append_rls "equation_prls" Celem.e_rls  [Celem.Calc ("Tools.matches",eval_matches "")],
    1.23 +        Rule.append_rls "equation_prls" Rule.e_rls  [Rule.Calc ("Tools.matches",eval_matches "")],
    1.24          SOME "solve (e_e::bool, v_v)", [])),
    1.25      (Specify.prep_pbt thy "pbl_equ_univ" [] Celem.e_pblID
    1.26        (["univariate","equation"],
    1.27 @@ -88,8 +88,8 @@
    1.28  setup {* KEStore_Elems.add_mets
    1.29    [Specify.prep_met thy "met_equ" [] Celem.e_metID
    1.30  	    (["Equation"], [],
    1.31 -	      {rew_ord'="tless_true", rls'=Celem.Erls, calc = [], srls = Celem.e_rls, prls=Celem.e_rls, crls = Atools_erls,
    1.32 -          errpats = [], nrls = Celem.e_rls},
    1.33 +	      {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,
    1.34 +          errpats = [], nrls = Rule.e_rls},
    1.35          "empty_script")]
    1.36  *}
    1.37