wneuper/isa: comparison src/Tools/isac/Knowledge/PolyMinus.thy

equal deleted inserted replaced

-:f2b3681fafb9
+:3e904f8ec16c
 klammer_minus_minus:         "a - (b - c) = (a - b) + c" and
 klammer_mult_minus:          "a * (b - c) = a * b - a * c" and
 klammer_minus_mult:          "(b - c) * a = b * a - c * a"
-ML {*
+ML \<open>
 val thy = @{theory};
 (** eval functions **)
 (*. get the identifier from specific monomials; see fun ist_monom .*)
 Rule.append_rls "rechnen" Rule.e_rls
 	       [Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
 		Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
 		Rule.Calc ("Groups.minus_class.minus", eval_binop "#subtr_")
 		];
-*}
+\<close>
-setup {* KEStore_Elems.add_rlss
+setup \<open>KEStore_Elems.add_rlss
 [("ordne_alphabetisch", (Context.theory_name @{theory}, prep_rls' ordne_alphabetisch)),
 ("fasse_zusammen", (Context.theory_name @{theory}, prep_rls' fasse_zusammen)),
 ("verschoenere", (Context.theory_name @{theory}, prep_rls' verschoenere)),
 ("ordne_monome", (Context.theory_name @{theory}, prep_rls' ordne_monome)),
 ("klammern_aufloesen", (Context.theory_name @{theory}, prep_rls' klammern_aufloesen)),
 ("klammern_ausmultiplizieren",
-(Context.theory_name @{theory}, prep_rls' klammern_ausmultiplizieren))] *}
+(Context.theory_name @{theory}, prep_rls' klammern_ausmultiplizieren))]\<close>
 (** problems **)
-setup {* KEStore_Elems.add_pbts
+setup \<open>KEStore_Elems.add_pbts
 [(Specify.prep_pbt thy "pbl_vereinf_poly" [] Celem.e_pblID
 (["polynom","vereinfachen"], [], Rule.Erls, NONE, [])),
 (Specify.prep_pbt thy "pbl_vereinf_poly_minus" [] Celem.e_pblID
 (["plus_minus","polynom","vereinfachen"],
 [("#Given", ["Term t_t"]),
 [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
 ("#Where" ,["e_e is_ratpolyexp"]),
 ("#Find"  ,["Geprueft p_p"])],
 Rule.append_rls "prls_pbl_probe_bruch" Rule.e_rls [(*for preds in where_*)
 		      Rule.Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
-SOME "Probe e_e w_w", [["probe","fuer_bruch"]]))] *}
+SOME "Probe e_e w_w", [["probe","fuer_bruch"]]))]\<close>
 (** methods **)
-setup {* KEStore_Elems.add_mets
+setup \<open>KEStore_Elems.add_mets
 [Specify.prep_met thy "met_simp_poly_minus" [] Celem.e_metID
 	    (["simplification","for_polynomials","with_minus"],
 	      [("#Given" ,["Term t_t"]),
 	        ("#Where" ,["t_t is_polyexp",
 	            "Not (matchsub (?a + (?b + ?c)) t_t | " ^
 	      {rew_ord'="tless_true", rls' = Rule.e_rls, calc = [], srls = Rule.e_rls,
 	        prls = Rule.append_rls "prls_met_probe_bruch" Rule.e_rls
 	            [(*for preds in where_*) Rule.Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
 	        crls = Rule.e_rls, errpats = [], nrls = Rule.Erls},
 	      "empty_script")]
-*}
+\<close>
 end

changeset 59472	3e904f8ec16c
parent 59416	229e5c9cf78b
child 59473	28b67cae58c3